From 38e5415604cb93e919b28e100da3200a95706244 Mon Sep 17 00:00:00 2001 From: MRHMisu Date: Sat, 27 Jun 2026 23:06:45 -0700 Subject: [PATCH 1/3] agent_harness flow works --- agent_harness/README.md | 175 ++ agent_harness/__init__.py | 12 + agent_harness/scaffold.py | 327 ++++ agent_harness/templates/AGENTS.md.tmpl | 70 + .../templates/AGENTS_no_harness.md.tmpl | 56 + agent_harness/templates/_env.sh | 32 + agent_harness/templates/cli.py | 387 ++++ agent_harness/templates/collect.py | 113 ++ agent_harness/templates/harness_tool.py | 1667 +++++++++++++++++ agent_harness/templates/requirements.txt | 1 + agent_harness/templates/root_README.md.tmpl | 74 + agent_harness/templates/run_agents.py | 172 ++ agent_harness/templates/run_specharness.sh | 6 + agent_harness/templates/score_all.py | 150 ++ agent_harness/templates/submit.sh | 6 + agent_harness/templates/verifier_tool.py | 283 +++ agent_harness/templates/verify.sh | 6 + 17 files changed, 3537 insertions(+) create mode 100644 agent_harness/README.md create mode 100644 agent_harness/__init__.py create mode 100644 agent_harness/scaffold.py create mode 100644 agent_harness/templates/AGENTS.md.tmpl create mode 100644 agent_harness/templates/AGENTS_no_harness.md.tmpl create mode 100644 agent_harness/templates/_env.sh create mode 100644 agent_harness/templates/cli.py create mode 100644 agent_harness/templates/collect.py create mode 100644 agent_harness/templates/harness_tool.py create mode 100644 agent_harness/templates/requirements.txt create mode 100644 agent_harness/templates/root_README.md.tmpl create mode 100644 agent_harness/templates/run_agents.py create mode 100644 agent_harness/templates/run_specharness.sh create mode 100644 agent_harness/templates/score_all.py create mode 100644 agent_harness/templates/submit.sh create mode 100644 agent_harness/templates/verifier_tool.py create mode 100644 agent_harness/templates/verify.sh diff --git a/agent_harness/README.md b/agent_harness/README.md new file mode 100644 index 0000000..f538a3b --- /dev/null +++ b/agent_harness/README.md @@ -0,0 +1,175 @@ +# agent_harness + +Expose VeriAct's four tools as standalone CLIs and scaffold a self-contained +working directory per benchmark task, so external coding agents (Codex, Claude +Code) can solve the same JML-spec-synthesis tasks with the same tools, prompt, and +success threshold as VeriAct — enabling an apples-to-apples comparison. + +The tools (mirroring `veriact/tools.py` + `default_tools.py`), with `analyze` +folded into `verify` so a single verification call returns the error analysis too: + +| CLI subcommand | VeriAct tool(s) | Output | +|----------------|-----------------|--------| +| `verify` | `verify_with_openjml` + `analyze_openjml_errors` | `{verified, return_code, errors, failure_modes, repair_hints, summary, raw_output}` | +| `harness` | `run_spec_harness` | `{task_id: {post_correctness, post_completeness, pre_correctness, pre_completeness}}` | +| `submit` | `task_complete` | writes `submission.json` (the comparison artifact) | + +This package is **self-contained**: `templates/` vendors the scoring/verification +code (`harness_tool.py`, `verifier_tool.py`) and the CLI, so it can live in its own +repository with no dependency on `veriact/`. Generated dirs need only the +`javalang` pip package and the `openjml` binary. + +## Scaffold + +```bash +# SpecGenBench — all 120 tasks +python -m agent_harness.scaffold \ + --benchmark benchmarks/specgenbench/sgb.json --out-root out/sgb + +# FormalBench — 120 tasks matching SGB's per-category distribution +python -m agent_harness.scaffold \ + --benchmark benchmarks/formalbench/fb.json --out-root out/fb \ + --sample-n 120 --match-distribution benchmarks/specgenbench/sgb.json --seed 0 +``` + +Each task dir gets exactly **5** IO pairs: from `test_inputs` first, topped up from +`generated_test_cases` (same selection the harness scores with `max_pairs=5`). + +### Attempt budget (stopping criterion) + +Each task has a fixed budget of tool attempts (`verify` + `harness` calls combined), +enforced by the vendored CLI so it's identical across VeriAct / Claude Code / Codex. +Set it at scaffold time with `--max-attempts N` (default **15**, matching VeriAct's +`--max-steps`; `0` = unlimited); it is stored in each dir's `harness/config.json` +and can be overridden per run with `AGENT_MAX_ATTEMPTS`. When the budget is reached +the tools refuse further calls and tell the agent to submit; `attempts` is recorded +in `submission.json`. + +### Ablation: with vs without the harness tool + +Pass `--no-harness` to scaffold an ablation arm where the agent works with +`verify` + `submit` only (no `run_specharness.sh`, and a harness-free `AGENTS.md` +whose success criterion is "verification passes"): + +```bash +python -m agent_harness.scaffold \ + --benchmark benchmarks/specgenbench/sgb.json --out-root out/sgb_no_harness --no-harness +``` + +`harness/cli.py` is still vendored in this arm, so after the agents finish you score +their generated JML with the spec-harness they never had — `score_all.py` (dropped +into every out-root) runs it over every dir's `Solution.java`: + +```bash +VERIACT_PYTHON=.venv/bin/python OPENJML=/path/to/openjml \ + python out/sgb_no_harness/score_all.py --threads 8 +# -> out/sgb_no_harness/harness_scores.{json,csv} and fills each submission.json +``` + +(`collect.py --score-missing` does the same on the fly for submissions still lacking +scores.) Run both arms (with- and without-harness) and diff the score tables to +measure the harness tool's effect on spec quality. + +## Run agents + compare + +From an out-root: + +```bash +python run_agents.py --agent claude --threads 4 # fan out, 1 session per task +python collect.py # comparison.json / comparison.csv +``` + +See the generated `out-root/README.md` for the per-root details. + +## Running in a `screen` session + +Batch runs are long, so launch them inside `screen` (or `tmux`) and detach. The +driver fans out one session per task dir; export `VERIACT_PYTHON` / `OPENJML` so +the tool scripts skip venv bootstrapping and find OpenJML. Per-task agent logs land +in `/harness/agent_run.log`; the `tee` below also captures the driver log. + +`screen` cheat-sheet: detach `Ctrl-a d` · reattach `screen -r ` · list +`screen -ls` · kill `screen -X -S quit`. + +### Claude Code + +`claude -p ""` runs headless and exits. For an unattended batch it must edit +files and run the `*.sh` tools without prompting, so pass +`--dangerously-skip-permissions` (only inside an isolated/sandboxed host). The driver +substitutes `{agents_md}` with each dir's `AGENTS.md`: + +```bash +screen -dmS sgb_claude bash -lc ' + cd /path/to/out/sgb + export VERIACT_PYTHON=/path/to/.venv/bin/python OPENJML=/path/to/openjml + python run_agents.py --threads 4 --timeout 1800 \ + --cmd "claude -p {agents_md} --dangerously-skip-permissions --model claude-opus-4-8" \ + 2>&1 | tee run_claude.log +' +screen -r sgb_claude # watch progress +``` + +To run a **single** task interactively instead, just work inside its dir: + +```bash +screen -S one_task +cd /path/to/out/sgb/SGB_Abs +export VERIACT_PYTHON=/path/to/.venv/bin/python OPENJML=/path/to/openjml +claude --dangerously-skip-permissions # then paste/point it at AGENTS.md +# detach with Ctrl-a d +``` + +### Codex + +`codex exec ""` runs non-interactively. Add `--skip-git-repo-check` (the task +dirs aren't git repos) and `--dangerously-bypass-approvals-and-sandbox` to disable +Codex's bubblewrap sandbox — in many containers/VMs bwrap cannot create its loopback +(`RTM_NEWADDR: Operation not permitted`), which makes every edit/command fail; the +bypass is the working path on an already-isolated host (and mirrors the claude +default). The built-in `--agent codex` does **not** pass `-m` — set your model in +`~/.codex/config.toml` (e.g. `model = "gpt-4o"`, which needs an OpenAI API-key login; +a ChatGPT-account login rejects `gpt-4o`). Override per run with `--cmd '... -m +...'`. + +```bash +screen -dmS sgb_codex bash -lc ' + cd /path/to/out/sgb + export VERIACT_PYTHON=/path/to/.venv/bin/python OPENJML=/path/to/openjml + python run_agents.py --agent codex --threads 4 --timeout 1800 \ + 2>&1 | tee run_codex.log +' +screen -r sgb_codex +``` + +After either run completes, aggregate with `python collect.py` (add +`--score-missing` for a `--no-harness` root). Use a **separate out-root per agent** +(scaffold twice, or copy the root) so their `submission.json` / `comparison.csv` +don't overwrite each other, then diff the tables. + +> Agent CLI flags change over time — if `--dangerously-skip-permissions`, +> `--full-auto`, or the model id differ in your install, adjust the `--cmd` string; +> the `{agents_md}` / `{agents_md_path}` / `{task_dir}` / `{task_id}` tokens stay the +> same. + +## Layout of this package + +``` +agent_harness/ +├── scaffold.py # generator (selection, 5-pair pick, stratified sampling) +├── templates/ +│ ├── cli.py # the 4-subcommand CLI (vendored into each dir's harness/) +│ ├── harness_tool.py # vendored scorer (copy of veriact/harness_tool.py) +│ ├── verifier_tool.py # vendored verifier (copy of veriact/verifier_tool.py) +│ ├── _env.sh # interpreter resolver / venv bootstrap +│ ├── verify.sh run_specharness.sh submit.sh +│ ├── AGENTS.md.tmpl AGENTS_no_harness.md.tmpl # per-task prompt (both arms) +│ ├── requirements.txt # javalang +│ ├── run_agents.py collect.py score_all.py # parent-root helpers +│ └── root_README.md.tmpl +└── README.md +``` + +> **Keeping the vendored copies in sync:** `templates/harness_tool.py` and +> `templates/verifier_tool.py` are verbatim copies of the same-named files in +> `veriact/`. If those change while this package still lives in the VeriAct repo, +> re-copy them. Once split into its own repo, `templates/` is the source of truth. diff --git a/agent_harness/__init__.py b/agent_harness/__init__.py new file mode 100644 index 0000000..42226ba --- /dev/null +++ b/agent_harness/__init__.py @@ -0,0 +1,12 @@ +"""agent_harness — expose VeriAct's four tools as standalone CLIs and scaffold +self-contained per-task working directories so external coding agents (Codex, +Claude Code) can solve the same JML-spec-synthesis tasks with the same tools. + +Modules +------- +cli : 4-subcommand tool dispatcher (verify | analyze | harness | submit) + — vendored into each generated task dir's ``harness/``. +scaffold : generator that materializes one self-contained dir per benchmark task. +run_agents : parent-level driver that fans out one agent session per task dir. +collect : aggregates every ``submission.json`` into a comparison table. +""" diff --git a/agent_harness/scaffold.py b/agent_harness/scaffold.py new file mode 100644 index 0000000..667c205 --- /dev/null +++ b/agent_harness/scaffold.py @@ -0,0 +1,327 @@ +#!/usr/bin/env python3 +"""Scaffold self-contained per-task working directories from a benchmark. + +For each selected benchmark task this creates a directory (named by ``task_id``) +containing the reference ``Solution.java``, ``Test.java``, exactly five IO pairs +under ``tests/``, a vendored ``harness/`` (the four-tool CLI + its dependencies), +the four ``*.sh`` tool wrappers, and an ``AGENTS.md`` instruction file. It then +drops parent-root helpers (``run_agents.py``, ``collect.py``, ``README.md``) so +the whole out-root can be handed to an external coding agent. + +The package is self-contained: it copies everything from ``templates/`` and never +imports ``veriact``, so it can live in its own repository. + +Examples +-------- + # SpecGenBench — all 120 tasks + python -m agent_harness.scaffold \ + --benchmark benchmarks/specgenbench/sgb.json --out-root out/sgb + + # FormalBench — 120 tasks matching SGB's per-category distribution + python -m agent_harness.scaffold \ + --benchmark benchmarks/formalbench/fb.json --out-root out/fb \ + --sample-n 120 --match-distribution benchmarks/specgenbench/sgb.json --seed 0 +""" + +from __future__ import annotations + +import argparse +import collections +import json +import os +import random +import shutil +import stat +import sys + +TEMPLATES = os.path.join(os.path.dirname(os.path.abspath(__file__)), "templates") + +# Files vendored into each task dir's harness/ (verbatim copies). +HARNESS_FILES = [ + "cli.py", + "harness_tool.py", + "verifier_tool.py", + "_env.sh", + "requirements.txt", +] +# Wrapper scripts written into each task dir (verbatim copies, made executable). +# run_specharness.sh is only included when scaffolding *with* the harness tool. +WRAPPER_FILES_BASE = ["verify.sh", "submit.sh"] +HARNESS_WRAPPER = "run_specharness.sh" +# Parent-root helpers dropped once into the out-root. +ROOT_FILES = ["run_agents.py", "collect.py", "score_all.py"] + +MAX_PAIRS = 5 + + +# --------------------------------------------------------------------------- +# benchmark loading / selection +# --------------------------------------------------------------------------- + +def load_benchmark(path: str) -> list[dict]: + with open(path) as fh: + raw = fh.read().strip() + if not raw: + return [] + if path.endswith(".jsonl") or (raw[0] != "[" and "\n" in raw): + records = [] + for line in raw.splitlines(): + line = line.strip() + if line: + records.append(json.loads(line)) + return records + return json.loads(raw) + + +def stratified_sample( + tasks: list[dict], + target_counts: dict[str, int], + seed: int, + key: str = "category", +) -> list[dict]: + """Pick tasks so per-category counts match *target_counts* exactly.""" + rng = random.Random(seed) + by_cat: dict[str, list[dict]] = collections.defaultdict(list) + for t in tasks: + by_cat[t.get(key, "")].append(t) + + chosen: list[dict] = [] + for cat, want in target_counts.items(): + pool = list(by_cat.get(cat, [])) + rng.shuffle(pool) + if len(pool) < want: + print( + f"WARNING: category '{cat}' has {len(pool)} tasks but " + f"{want} requested; taking all available.", + file=sys.stderr, + ) + chosen.extend(pool[:want]) + rng.shuffle(chosen) + return chosen + + +def proportional_sample( + tasks: list[dict], n: int, seed: int, key: str = "category" +) -> list[dict]: + """Pick *n* tasks proportional to the dataset's own category distribution.""" + rng = random.Random(seed) + by_cat: dict[str, list[dict]] = collections.defaultdict(list) + for t in tasks: + by_cat[t.get(key, "")].append(t) + total = len(tasks) + chosen: list[dict] = [] + for cat, pool in by_cat.items(): + pool = list(pool) + rng.shuffle(pool) + want = round(n * len(pool) / total) + chosen.extend(pool[:want]) + rng.shuffle(chosen) + return chosen[:n] + + +def select_tasks(tasks: list[dict], args: argparse.Namespace) -> list[dict]: + if args.task_id: + sel = [t for t in tasks if t.get("task_id") == args.task_id] + if not sel: + sys.exit(f"task_id '{args.task_id}' not found in benchmark") + return sel + + if args.task_ids: + with open(args.task_ids) as fh: + wanted = {ln.strip() for ln in fh if ln.strip()} + return [t for t in tasks if t.get("task_id") in wanted] + + if args.match_distribution: + ref = load_benchmark(args.match_distribution) + counts = collections.Counter(t.get("category", "") for t in ref) + return stratified_sample(tasks, dict(counts), args.seed) + + if args.sample_n: + return proportional_sample(tasks, args.sample_n, args.seed) + + if args.limit: + return tasks[: args.limit] + + return tasks + + +# --------------------------------------------------------------------------- +# per-task scaffolding +# --------------------------------------------------------------------------- + +def pick_pairs(task: dict, max_pairs: int = MAX_PAIRS) -> list[dict]: + """Exactly *max_pairs* IO pairs: test_inputs first, then generated_test_cases.""" + pairs = list(task.get("test_inputs", []))[:max_pairs] + if len(pairs) < max_pairs: + need = max_pairs - len(pairs) + pairs.extend(list(task.get("generated_test_cases", []))[:need]) + return pairs + + +def _safe_name(task_id: str) -> str: + return task_id.replace("/", "_").replace("\\", "_") + + +def _write(path: str, content: str, executable: bool = False) -> None: + with open(path, "w") as fh: + fh.write(content) + if executable: + mode = os.stat(path).st_mode + os.chmod(path, mode | stat.S_IXUSR | stat.S_IXGRP | stat.S_IXOTH) + + +def _render(template_name: str, mapping: dict[str, str]) -> str: + with open(os.path.join(TEMPLATES, template_name)) as fh: + text = fh.read() + for k, v in mapping.items(): + text = text.replace("{{" + k + "}}", v) + return text + + +def scaffold_task( + task: dict, + out_root: str, + threshold: float, + with_harness: bool = True, + max_attempts: int = 15, +) -> str: + task_id = task["task_id"] + task_dir = os.path.join(out_root, _safe_name(task_id)) + harness_dir = os.path.join(task_dir, "harness") + tests_dir = os.path.join(task_dir, "tests") + os.makedirs(harness_dir, exist_ok=True) + os.makedirs(tests_dir, exist_ok=True) + + # Source files the agent works on / reads. + _write(os.path.join(task_dir, "Solution.java"), task.get("code", "")) + _write(os.path.join(task_dir, "Test.java"), task.get("test_code", "")) + + # Exactly-5 IO pairs. + pairs = pick_pairs(task) + for i, pair in enumerate(pairs): + _write( + os.path.join(tests_dir, f"case_{i}.json"), + json.dumps({"input": pair["input"], "output": pair["output"]}, indent=2), + ) + + # Authoritative task record for the harness CLI: the chosen 5 pairs as + # test_inputs, generated_test_cases emptied (so scoring == tests/). + task_record = dict(task) + task_record["test_inputs"] = pairs + task_record["generated_test_cases"] = [] + _write(os.path.join(harness_dir, "task.json"), json.dumps(task_record, indent=2)) + + # Per-task tool config (attempt budget). $AGENT_MAX_ATTEMPTS overrides at runtime. + _write( + os.path.join(harness_dir, "config.json"), + json.dumps({"max_attempts": max_attempts}, indent=2), + ) + + # Vendored harness files (cli.py is always present so the harness CLI can be + # run offline for scoring, even in the no-harness ablation arm). + for name in HARNESS_FILES: + shutil.copy2(os.path.join(TEMPLATES, name), os.path.join(harness_dir, name)) + + # Executable wrappers — run_specharness.sh only in the with-harness arm. + wrappers = list(WRAPPER_FILES_BASE) + if with_harness: + wrappers.insert(1, HARNESS_WRAPPER) + for name in wrappers: + dst = os.path.join(task_dir, name) + shutil.copy2(os.path.join(TEMPLATES, name), dst) + mode = os.stat(dst).st_mode + os.chmod(dst, mode | stat.S_IXUSR | stat.S_IXGRP | stat.S_IXOTH) + + # Instruction file — harness-aware vs harness-free variant. + template = "AGENTS.md.tmpl" if with_harness else "AGENTS_no_harness.md.tmpl" + agents_md = _render( + template, + { + "TASK_ID": task_id, + "THRESHOLD": f"{threshold:g}", + "MAX_ATTEMPTS": str(max_attempts), + "SOLUTION_CODE": task.get("code", ""), + }, + ) + _write(os.path.join(task_dir, "AGENTS.md"), agents_md) + return task_dir + + +def write_root_helpers( + out_root: str, benchmark: str, n_tasks: int, with_harness: bool = True +) -> None: + for name in ROOT_FILES: + dst = os.path.join(out_root, name) + shutil.copy2(os.path.join(TEMPLATES, name), dst) + if name.endswith(".py"): + mode = os.stat(dst).st_mode + os.chmod(dst, mode | stat.S_IXUSR | stat.S_IXGRP | stat.S_IXOTH) + readme = _render( + "root_README.md.tmpl", + { + "BENCHMARK": os.path.basename(benchmark), + "N_TASKS": str(n_tasks), + "MODE": "with-harness" if with_harness else "no-harness (ablation)", + }, + ) + _write(os.path.join(out_root, "README.md"), readme) + + +# --------------------------------------------------------------------------- +# CLI +# --------------------------------------------------------------------------- + +def build_parser() -> argparse.ArgumentParser: + p = argparse.ArgumentParser(description="Scaffold per-task agent working dirs.") + p.add_argument("--benchmark", required=True, help="benchmark .json/.jsonl path") + p.add_argument("--out-root", required=True, help="output root directory") + p.add_argument("--task-id", help="scaffold a single task by id") + p.add_argument("--task-ids", help="file with task ids (one per line)") + p.add_argument("--limit", type=int, help="scaffold only the first N tasks") + p.add_argument("--sample-n", type=int, help="sample N tasks (proportional by category)") + p.add_argument( + "--match-distribution", + help="benchmark whose per-category counts the sample should match", + ) + p.add_argument("--stratify-by", default="category", help="record key to stratify on") + p.add_argument("--seed", type=int, default=0, help="sampling seed (default: 0)") + p.add_argument("--threshold", type=float, default=0.50, help="pass threshold") + p.add_argument( + "--no-harness", + action="store_true", + help="ablation: omit the run_spec_harness tool from the dirs and use a " + "harness-free AGENTS.md (agent works with verify + submit only)", + ) + p.add_argument( + "--max-attempts", + type=int, + default=15, + help="attempt budget per task (verify+harness calls; 0 = unlimited; " + "default: 15, matching VeriAct --max-steps)", + ) + return p + + +def main(argv: list[str] | None = None) -> int: + args = build_parser().parse_args(argv) + tasks = load_benchmark(args.benchmark) + selected = select_tasks(tasks, args) + os.makedirs(args.out_root, exist_ok=True) + + with_harness = not args.no_harness + for task in selected: + scaffold_task( + task, args.out_root, args.threshold, with_harness, args.max_attempts + ) + write_root_helpers(args.out_root, args.benchmark, len(selected), with_harness) + + counts = collections.Counter(t.get(args.stratify_by, "") for t in selected) + mode = "with-harness" if with_harness else "no-harness (ablation)" + print(f"Scaffolded {len(selected)} task(s) [{mode}] -> {args.out_root}") + for cat, n in counts.most_common(): + print(f" {cat or '(none)'}: {n}") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/agent_harness/templates/AGENTS.md.tmpl b/agent_harness/templates/AGENTS.md.tmpl new file mode 100644 index 0000000..de27e8e --- /dev/null +++ b/agent_harness/templates/AGENTS.md.tmpl @@ -0,0 +1,70 @@ +# Task {{TASK_ID}} — Synthesize a JML specification + +You are an expert Formal Verification Engineer. Given the Java program in +`Solution.java`, write JML specifications (`requires`, `ensures`, and any +`loop_invariant` / `assignable` / `decreases` needed) and iteratively verify them +with OpenJML until they pass and score well on the spec-harness. + +Work in a **verify → fix → score → submit** loop, using the three tools below +(all are shell scripts in this directory). + +## Rules + +- Edit **`Solution.java`** in place. Keep the method body unchanged; only add JML + annotations. The class **MUST** stay named `Solution`. +- `Test.java` and `tests/case_*.json` show how inputs/outputs are formatted — read + them to understand the method's behavior. Do not edit them. +- Run every tool from **this directory**. +- You have a budget of **{{MAX_ATTEMPTS}}** tool attempts (`verify` + `run_specharness` + calls combined). Each call reports `attempts`/`max_attempts`. When the budget is + exhausted the tools refuse and you must call `./submit.sh` with your best spec. + +## Tools + +### `./verify.sh` +Run OpenJML Extended Static Checking on `Solution.java`, **with built-in error +analysis**. Prints JSON: +`{"verified": bool, "return_code": int, "errors": [{"type","raw"}], "failure_modes": [...], "repair_hints": [...], "summary": str, "raw_output": str}` +and saves it to `harness/last_verify.json`. +Use at every verification attempt; read `repair_hints`/`summary` to fix failures. If +`raw_output` contains `Timeout`: STOP and **simplify** the spec before retrying — +never resubmit a structurally identical spec after a timeout. + +### `./run_specharness.sh` +Evaluate spec quality on four metrics in `[0.0, 1.0]` (1.0 = perfect): +- `post_correctness` — `ensures` holds on all test inputs +- `post_completeness` — `ensures` is tight enough to kill output mutants +- `pre_correctness` — `requires` does not reject valid inputs +- `pre_completeness` — `requires` rejects invalid inputs + +Prints JSON: `{"{{TASK_ID}}": {post_correctness, post_completeness, pre_correctness, pre_completeness}}`. +Call **after** verification passes. + +### `./submit.sh "summary"` +Record your final submission (writes `submission.json` with the final code, last +scores, and a `passed` flag). Call once you meet the success threshold. + +## Workflow + +1. Read `Solution.java`, `Test.java`, and a few `tests/case_*.json`. Infer behavior. +2. Add JML to `Solution.java`. +3. `./verify.sh` + - failed → read `repair_hints`/`summary`, refine the spec, go to 3. + - timeout → simplify the spec, go to 3. + - passed → continue. +4. `./run_specharness.sh` + - If `post_correctness >= {{THRESHOLD}}` **AND** `post_completeness >= {{THRESHOLD}}`: + call `./submit.sh` **immediately**. Do NOT refine further. + - Else refine the spec (low `post_correctness` → fix `ensures`; low + `post_completeness` → add constraints to `ensures`) and go to 3. + +## Success criterion + +`post_correctness >= {{THRESHOLD}}` AND `post_completeness >= {{THRESHOLD}}`. +Once both meet the threshold, submit right away. + +## The program + +```java +{{SOLUTION_CODE}} +``` diff --git a/agent_harness/templates/AGENTS_no_harness.md.tmpl b/agent_harness/templates/AGENTS_no_harness.md.tmpl new file mode 100644 index 0000000..2df155c --- /dev/null +++ b/agent_harness/templates/AGENTS_no_harness.md.tmpl @@ -0,0 +1,56 @@ +# Task {{TASK_ID}} — Synthesize a JML specification + +You are an expert Formal Verification Engineer. Given the Java program in +`Solution.java`, write JML specifications (`requires`, `ensures`, and any +`loop_invariant` / `assignable` / `decreases` needed) and iteratively verify them +with OpenJML until they pass. + +Work in a **verify → fix → submit** loop, using the two tools below (both are +shell scripts in this directory). + +## Rules + +- Edit **`Solution.java`** in place. Keep the method body unchanged; only add JML + annotations. The class **MUST** stay named `Solution`. +- `Test.java` and `tests/case_*.json` show how inputs/outputs are formatted — read + them to understand the method's behavior. Do not edit them. +- Run every tool from **this directory**. +- You have a budget of **{{MAX_ATTEMPTS}}** `verify` attempts. Each call reports + `attempts`/`max_attempts`. When the budget is exhausted `verify` refuses and you + must call `./submit.sh` with your best spec. + +## Tools + +### `./verify.sh` +Run OpenJML Extended Static Checking on `Solution.java`, **with built-in error +analysis**. Prints JSON: +`{"verified": bool, "return_code": int, "errors": [{"type","raw"}], "failure_modes": [...], "repair_hints": [...], "summary": str, "raw_output": str}` +and saves it to `harness/last_verify.json`. +Use at every verification attempt; read `repair_hints`/`summary` to fix failures. If +`raw_output` contains `Timeout`: STOP and **simplify** the spec before retrying — +never resubmit a structurally identical spec after a timeout. + +### `./submit.sh "summary"` +Record your final submission (writes `submission.json` with the final code). Call +once verification passes. + +## Workflow + +1. Read `Solution.java`, `Test.java`, and a few `tests/case_*.json`. Infer behavior. +2. Add JML to `Solution.java`. Aim for a spec that is both **correct** (true for the + method) and **strong** (captures the full input/output relationship), not a + trivially-true one. +3. `./verify.sh` + - failed → read `repair_hints`/`summary`, refine the spec, go to 3. + - timeout → simplify the spec, go to 3. + - passed → `./submit.sh "..."` and stop. + +## Success criterion + +`./verify.sh` reports `"verified": true`. Submit your strongest verifying spec. + +## The program + +```java +{{SOLUTION_CODE}} +``` diff --git a/agent_harness/templates/_env.sh b/agent_harness/templates/_env.sh new file mode 100644 index 0000000..82d81f0 --- /dev/null +++ b/agent_harness/templates/_env.sh @@ -0,0 +1,32 @@ +#!/usr/bin/env bash +# Resolve a Python interpreter that can `import javalang`; bootstrap a local +# venv on first use if none is available. Sets and exports $PYTHON. +# Sourced by the task-dir wrapper scripts (verify.sh, analyze.sh, ...). +set -euo pipefail + +_HARNESS_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" + +if [ -n "${VERIACT_PYTHON:-}" ]; then + PYTHON="$VERIACT_PYTHON" +elif python -c 'import javalang' >/dev/null 2>&1; then + PYTHON="python" +elif python3 -c 'import javalang' >/dev/null 2>&1; then + PYTHON="python3" +elif [ -x "$_HARNESS_DIR/.venv/bin/python" ]; then + PYTHON="$_HARNESS_DIR/.venv/bin/python" +else + echo "[agent_harness] bootstrapping venv at $_HARNESS_DIR/.venv ..." >&2 + if command -v uv >/dev/null 2>&1; then + uv venv "$_HARNESS_DIR/.venv" >&2 + uv pip install --python "$_HARNESS_DIR/.venv/bin/python" \ + -r "$_HARNESS_DIR/requirements.txt" >&2 + else + python3 -m venv "$_HARNESS_DIR/.venv" >&2 + "$_HARNESS_DIR/.venv/bin/python" -m pip install -q --upgrade pip >&2 + "$_HARNESS_DIR/.venv/bin/python" -m pip install -q \ + -r "$_HARNESS_DIR/requirements.txt" >&2 + fi + PYTHON="$_HARNESS_DIR/.venv/bin/python" +fi + +export PYTHON diff --git a/agent_harness/templates/cli.py b/agent_harness/templates/cli.py new file mode 100644 index 0000000..eceb136 --- /dev/null +++ b/agent_harness/templates/cli.py @@ -0,0 +1,387 @@ +#!/usr/bin/env python3 +"""agent_harness CLI — VeriAct's four tools as a single command-line dispatcher. + +This file is *vendored* into each generated task directory as ``harness/cli.py``. +It imports its sibling modules ``harness_tool`` and ``verifier_tool`` (also +vendored) so the task directory is fully self-contained: the only external +requirements are the ``javalang`` pip package and the ``openjml`` binary. + +Subcommands +----------- + verify run OpenJML ESC on Solution.java; the result also includes the + error analysis (failure modes + repair hints) + harness score the spec on the four spec-harness metrics + submit record the final submission (the comparison artifact) + +Paths are resolved relative to this file: ``harness/`` is this file's directory +and the task directory is its parent (which holds ``Solution.java``). +""" + +from __future__ import annotations + +import argparse +import json +import os +import sys + +# This file lives at /harness/cli.py +HARNESS_DIR = os.path.dirname(os.path.abspath(__file__)) +TASK_DIR = os.path.dirname(HARNESS_DIR) + +# Make the vendored sibling modules importable regardless of cwd. +if HARNESS_DIR not in sys.path: + sys.path.insert(0, HARNESS_DIR) + +from harness_tool import Task, evaluate_problem # noqa: E402 +from verifier_tool import ( # noqa: E402 + VerificationResult, + verify_with_openjml, +) + +# Repair hints — copied from veriact/tools.py so the dir stays self-contained. +REPAIR_HINTS: dict[str, str] = { + "SyntaxError": "Fix JML syntax (missing semicolons, wrong keywords).", + "PostconditionFailure": "The @ensures clause is logically incorrect.", + "ExceptionalPostconditionFailure": "The @signals clause is incorrect.", + "PreconditionFailure": "The @requires clause is too weak or wrong.", + "LoopInvariantFailure": "The @maintaining clause doesn't hold.", + "RankingFunctionFailure": "The @decreases expression is wrong.", + "AssignableFailure": "The @assignable clause is too permissive or missing.", + "ArrayIndex": "Missing array bounds check in @requires.", + "NegativeSize": "Array size may be negative; add check in @requires.", + "NullDeReference": "Missing null check in @requires.", + "NullUnbox": "Potential null unboxing; add null check in @requires.", + "DivideByZero": "Missing division-by-zero guard in @requires.", + "ArithmeticOperationRange": "Integer overflow not guarded in @requires.", + "ArithmeticCastRange": "Cast may overflow; add range guard in @requires.", + "BadCast": "Unsafe cast; add type guard in @requires.", + "BadArrayAssignment": "Incompatible array assignment; check element types.", + "CalledMethodPrecondition": "Called method precondition not met; strengthen @requires.", + "LargeShift": "Shift amount out of range; add bounds check in @requires.", + "AssertFailure": "An @assert statement fails; check the invariant.", + "UnknownVerificationFailure": "Unknown verification failure; review the full OpenJML log.", +} + +# Threshold for a "passed" submission (mirrors veriact HARNESS_PASS_THRESHOLD). +HARNESS_PASS_THRESHOLD = 0.50 + +# Sibling artifact paths. +TASK_JSON = os.path.join(HARNESS_DIR, "task.json") +CONFIG_JSON = os.path.join(HARNESS_DIR, "config.json") +LAST_VERIFY = os.path.join(HARNESS_DIR, "last_verify.json") +LAST_SCORES = os.path.join(HARNESS_DIR, "last_scores.json") +RUN_COUNTER = os.path.join(HARNESS_DIR, ".run_counter") +ATTEMPTS_FILE = os.path.join(HARNESS_DIR, ".attempts") +SUBMISSION = os.path.join(TASK_DIR, "submission.json") + +DEFAULT_MAX_ATTEMPTS = 15 + + +# --------------------------------------------------------------------------- +# helpers +# --------------------------------------------------------------------------- + +def _resolve_openjml(openjml: str) -> None: + """The vendored tools invoke the literal binary name ``openjml``. + + If a concrete path is supplied (via --openjml or $OPENJML), prepend its + directory to PATH so the literal ``openjml`` resolves to it. + """ + if openjml and openjml != "openjml" and os.sep in openjml: + d = os.path.dirname(os.path.abspath(openjml)) + os.environ["PATH"] = d + os.pathsep + os.environ.get("PATH", "") + + +def _default_openjml(arg: str | None) -> str: + return arg or os.environ.get("OPENJML", "openjml") + + +def _read_code(code_path: str | None) -> str: + path = code_path or os.path.join(TASK_DIR, "Solution.java") + with open(path) as fh: + return fh.read() + + +def _load_task() -> Task: + with open(TASK_JSON) as fh: + return Task.from_dict(json.load(fh)) + + +def _emit(obj) -> None: + print(json.dumps(obj, indent=2)) + + +# ---- attempt budget (shared across verify + harness) ---------------------- + +def _max_attempts() -> int: + """Per-task attempt cap: $AGENT_MAX_ATTEMPTS, else config.json, else default. + + A value <= 0 means unlimited. + """ + env = os.environ.get("AGENT_MAX_ATTEMPTS") + if env is not None: + try: + return int(env) + except ValueError: + pass + if os.path.exists(CONFIG_JSON): + try: + with open(CONFIG_JSON) as fh: + return int(json.load(fh).get("max_attempts", DEFAULT_MAX_ATTEMPTS)) + except (OSError, ValueError, json.JSONDecodeError): + pass + return DEFAULT_MAX_ATTEMPTS + + +def _read_attempts() -> int: + if os.path.exists(ATTEMPTS_FILE): + try: + with open(ATTEMPTS_FILE) as fh: + return int(fh.read().strip() or "0") + except (OSError, ValueError): + return 0 + return 0 + + +def _check_budget() -> dict | None: + """If the budget is exhausted return an error dict; otherwise consume one + attempt and return None.""" + mx = _max_attempts() + used = _read_attempts() + if mx > 0 and used >= mx: + return { + "error": f"attempt budget exhausted ({used}/{mx})", + "action": "call ./submit.sh with your best spec", + "attempts": used, + "max_attempts": mx, + } + with open(ATTEMPTS_FILE, "w") as fh: + fh.write(str(used + 1)) + return None + + +def _budget_info() -> dict: + mx = _max_attempts() + return {"attempts": _read_attempts(), "max_attempts": mx if mx > 0 else None} + + +def _analyze(classified_errors: list[dict]) -> dict: + """Turn OpenJML classified errors into failure modes + repair hints.""" + failure_modes: list[str] = [] + repair_hints: list[str] = [] + seen: set[str] = set() + for err in classified_errors: + ftype = err.get("type", "UnknownVerificationFailure") + failure_modes.append(ftype) + hint = REPAIR_HINTS.get(ftype) + if hint and ftype not in seen: + repair_hints.append(f"{ftype}: {hint}") + seen.add(ftype) + if failure_modes: + counts: dict[str, int] = {} + for fm in failure_modes: + counts[fm] = counts.get(fm, 0) + 1 + summary = ", ".join(f"{t} (x{c})" if c > 1 else t for t, c in counts.items()) + else: + summary = "No failures detected." + return { + "failure_modes": failure_modes, + "repair_hints": repair_hints, + "summary": summary, + } + + +# --------------------------------------------------------------------------- +# subcommands +# --------------------------------------------------------------------------- + +def cmd_verify(args: argparse.Namespace) -> int: + exhausted = _check_budget() + if exhausted is not None: + _emit(exhausted) + return 2 + _resolve_openjml(_default_openjml(args.openjml)) + code = _read_code(args.code) + try: + task = _load_task() + classname = task.class_name or "Solution" + except (OSError, KeyError, json.JSONDecodeError): + classname = "Solution" + + result: VerificationResult = verify_with_openjml( + code, + classname=classname, + output_dir=os.path.join(HARNESS_DIR, "tmp"), + ) + analysis = _analyze(result.classified_errors) + out = { + "verified": result.success, + "return_code": result.return_code, + "errors": result.classified_errors, + "failure_modes": analysis["failure_modes"], + "repair_hints": analysis["repair_hints"], + "summary": analysis["summary"], + "raw_output": result.error_log, + **_budget_info(), + } + with open(LAST_VERIFY, "w") as fh: + json.dump(out, fh, indent=2) + _emit(out) + return 0 + + +def _next_run_id() -> str: + n = 0 + if os.path.exists(RUN_COUNTER): + try: + with open(RUN_COUNTER) as fh: + n = int(fh.read().strip() or "0") + except (ValueError, OSError): + n = 0 + n += 1 + with open(RUN_COUNTER, "w") as fh: + fh.write(str(n)) + return f"run_{n}" + + +def cmd_harness(args: argparse.Namespace) -> int: + if not args.no_budget: + exhausted = _check_budget() + if exhausted is not None: + _emit(exhausted) + return 2 + openjml = _default_openjml(args.openjml) + _resolve_openjml(openjml) + code = _read_code(args.code) + try: + task = _load_task() + except (OSError, KeyError, json.JSONDecodeError) as exc: + _emit({"error": f"cannot load task.json: {exc}"}) + return 1 + + run_id = _next_run_id() + scores = evaluate_problem( + task, + llm_code=code, + openjml_path=openjml, + output_dir=HARNESS_DIR, + run_id=run_id, + max_pairs=args.max_pairs, + ) + if not scores: + _emit({"error": "No test pairs could be parsed.", "task_id": task.task_id}) + return 1 + + out = { + task.task_id: { + "post_correctness": scores.get("post_correctness", 0.0), + "post_completeness": scores.get("post_completeness", 0.0), + "pre_correctness": scores.get("pre_correctness", 0.0), + "pre_completeness": scores.get("pre_completeness", 0.0), + } + } + with open(LAST_SCORES, "w") as fh: + json.dump(out, fh, indent=2) + if not args.no_budget: + _emit({**out, "_budget": _budget_info()}) + else: + _emit(out) + return 0 + + +def cmd_submit(args: argparse.Namespace) -> int: + import datetime + + try: + task = _load_task() + task_id = task.task_id + except (OSError, KeyError, json.JSONDecodeError): + task_id = os.path.basename(TASK_DIR) + + final_code = "" + sol_path = os.path.join(TASK_DIR, "Solution.java") + if os.path.exists(sol_path): + with open(sol_path) as fh: + final_code = fh.read() + + scores = None + passed = False + if os.path.exists(LAST_SCORES): + with open(LAST_SCORES) as fh: + last = json.load(fh) + metrics = last.get(task_id) or next(iter(last.values()), {}) + if isinstance(metrics, dict): + scores = metrics + passed = ( + metrics.get("post_correctness", 0.0) >= HARNESS_PASS_THRESHOLD + and metrics.get("post_completeness", 0.0) >= HARNESS_PASS_THRESHOLD + ) + + submission = { + "task_id": task_id, + "summary": args.summary, + "final_code": final_code, + "scores": scores, + "passed": passed, + "threshold": HARNESS_PASS_THRESHOLD, + "attempts": _read_attempts(), + "max_attempts": _max_attempts() or None, + "timestamp": datetime.datetime.now().isoformat(timespec="seconds"), + } + with open(SUBMISSION, "w") as fh: + json.dump(submission, fh, indent=2) + _emit( + { + "submitted": True, + "task_id": task_id, + "passed": passed, + "scores": scores, + "path": SUBMISSION, + } + ) + return 0 + + +# --------------------------------------------------------------------------- +# argument parsing +# --------------------------------------------------------------------------- + +def build_parser() -> argparse.ArgumentParser: + p = argparse.ArgumentParser( + prog="harness/cli.py", + description="VeriAct tools: verify | analyze | harness | submit.", + ) + sub = p.add_subparsers(dest="command", required=True) + + pv = sub.add_parser( + "verify", + help="run OpenJML ESC (output includes failure modes + repair hints)", + ) + pv.add_argument("--code", help="path to Java source (default: ../Solution.java)") + pv.add_argument("--openjml", help="OpenJML binary path (default: $OPENJML or 'openjml')") + pv.set_defaults(func=cmd_verify) + + ph = sub.add_parser("harness", help="score the spec on the 4 spec-harness metrics") + ph.add_argument("--code", help="path to Java source (default: ../Solution.java)") + ph.add_argument("--openjml", help="OpenJML binary path (default: $OPENJML or 'openjml')") + ph.add_argument("--max-pairs", type=int, default=5, dest="max_pairs", + help="max test pairs to score (default: 5)") + ph.add_argument("--no-budget", action="store_true", + help="don't count this run against the attempt budget " + "(for offline experimenter scoring)") + ph.set_defaults(func=cmd_harness) + + ps = sub.add_parser("submit", help="record the final submission") + ps.add_argument("summary", help="brief summary of the final spec and scores") + ps.set_defaults(func=cmd_submit) + + return p + + +def main(argv: list[str] | None = None) -> int: + args = build_parser().parse_args(argv) + return args.func(args) + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/agent_harness/templates/collect.py b/agent_harness/templates/collect.py new file mode 100644 index 0000000..8b9c269 --- /dev/null +++ b/agent_harness/templates/collect.py @@ -0,0 +1,113 @@ +#!/usr/bin/env python3 +"""Aggregate every submission.json in this out-root into a comparison table. + +Writes ``comparison.json`` and ``comparison.csv`` summarizing each task's four +spec-harness scores and pass/fail. Run this after ``run_agents.py`` (or after an +agent has solved the dirs). Run it once per agent's out-root, then diff the +tables to compare VeriAct / Claude Code / Codex. + +Self-contained (stdlib only); ships inside the out-root. +""" + +from __future__ import annotations + +import argparse +import csv +import json +import os +import subprocess +import sys + +ROOT = os.path.dirname(os.path.abspath(__file__)) +METRICS = ["post_correctness", "post_completeness", "pre_correctness", "pre_completeness"] +THRESHOLD = 0.50 + + +def _score_offline(task_dir: str) -> dict | None: + """Run the vendored harness CLI on a dir's Solution.java (ablation arm). + + Honors $VERIACT_PYTHON (else 'python') and $OPENJML. Returns the metric dict + or None on failure. + """ + cli = os.path.join(task_dir, "harness", "cli.py") + if not os.path.exists(cli): + return None + python = os.environ.get("VERIACT_PYTHON", "python") + cmd = [python, cli, "harness", "--no-budget"] + if os.environ.get("OPENJML"): + cmd += ["--openjml", os.environ["OPENJML"]] + try: + out = subprocess.run( + cmd, cwd=task_dir, capture_output=True, text=True, timeout=1800 + ).stdout + data = json.loads(out) + metrics = next(iter(data.values()), None) + return metrics if isinstance(metrics, dict) and "error" not in data else None + except (subprocess.SubprocessError, json.JSONDecodeError, ValueError): + return None + + +def collect(score_missing: bool = False) -> list[dict]: + rows: list[dict] = [] + for name in sorted(os.listdir(ROOT)): + task_dir = os.path.join(ROOT, name) + sub = os.path.join(task_dir, "submission.json") + if not os.path.exists(sub): + continue + with open(sub) as fh: + data = json.load(fh) + scores = data.get("scores") or {} + if not scores and score_missing: + print(f" scoring {name} offline ...", file=sys.stderr) + scored = _score_offline(task_dir) + if scored: + scores = scored + data["passed"] = ( + scored.get("post_correctness", 0.0) >= THRESHOLD + and scored.get("post_completeness", 0.0) >= THRESHOLD + ) + row = { + "task_id": data.get("task_id", name), + "submitted": True, + "passed": bool(data.get("passed", False)), + } + for m in METRICS: + row[m] = scores.get(m) if isinstance(scores, dict) else None + rows.append(row) + return rows + + +def main(argv: list[str] | None = None) -> int: + p = argparse.ArgumentParser(description="Aggregate submissions into a comparison table.") + p.add_argument("--out", default=os.path.join(ROOT, "comparison"), + help="output path prefix (default: ./comparison)") + p.add_argument("--score-missing", action="store_true", + help="score submissions lacking scores via the vendored harness " + "CLI (for no-harness ablation roots; honors " + "$VERIACT_PYTHON / $OPENJML)") + args = p.parse_args(argv) + + rows = collect(score_missing=args.score_missing) + fields = ["task_id", "submitted", "passed", *METRICS] + + with open(args.out + ".json", "w") as fh: + json.dump(rows, fh, indent=2) + with open(args.out + ".csv", "w", newline="") as fh: + w = csv.DictWriter(fh, fieldnames=fields) + w.writeheader() + w.writerows(rows) + + n = len(rows) + passed = sum(1 for r in rows if r["passed"]) + avg = { + m: round(sum(r[m] for r in rows if r[m] is not None) / n, 3) if n else 0.0 + for m in METRICS + } + print(f"Collected {n} submission(s); passed={passed}") + print(f" avg: {avg}") + print(f" -> {args.out}.json / {args.out}.csv") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/agent_harness/templates/harness_tool.py b/agent_harness/templates/harness_tool.py new file mode 100644 index 0000000..afa7049 --- /dev/null +++ b/agent_harness/templates/harness_tool.py @@ -0,0 +1,1667 @@ +""" +harness_tool.py +--------------- +Self-contained module exposing ``evaluate_problem`` — a single entry-point +for evaluating one LLM-generated JML annotation against a benchmark Task. + +All dependencies from harness.py, eval_spec.py, and eval_llm_response.py +are inlined here so this file can be used as a standalone tool. + +Usage +----- + from harness_tool import evaluate_problem, Task, TestCase + + task = Task( + task_id="...", + code="...", # benchmark Solution.java source + class_name="Solution", + test_name="Test", + javadoc="...", + category="...", + origin_id="...", + test_code="...", # benchmark Test.java source + test_inputs=[TestCase(input="...", output="...")], + ) + result = evaluate_problem(task, llm_code="...", openjml_path="openjml") +""" + +from __future__ import annotations + +import logging +import os +import re +import json +import subprocess +import textwrap +import tempfile +from concurrent.futures import ThreadPoolExecutor, as_completed +from dataclasses import dataclass, field +from enum import Enum +from signal import signal +from typing import Any, Optional + +import javalang +import javalang.tree as jtree + +logger = logging.getLogger(__name__) + + + +# Result types (from harness.py) + +class VerifyResult(Enum): + OK = "ok" + FAIL = "fail" + UNKNOWN = "unknown" + + +@dataclass +class HarnessResult: + metric: str + total: int + passed: int + details: list = field(default_factory=list) + + @property + def score(self) -> float: + return self.passed / self.total if self.total > 0 else 0.0 + + def __str__(self) -> str: + return ( + f"{self.metric:25s} score={self.score:.3f}" + f" ({self.passed}/{self.total})" + ) + + + +# Test data structures (from harness.py) + +@dataclass +class TestPair: + """One concrete input-output pair for postcondition evaluation.""" + + inputs: dict[str, Any] # {"paramName": pythonValue, …} + output: Any # expected return value + label: str = "" + + +@dataclass +class InputCase: + """One input case for precondition evaluation.""" + + inputs: dict[str, Any] # {"paramName": pythonValue, …} + valid: bool # True → T+ (must be admitted by precondition) + # False → T- (must be rejected by precondition) + label: str = "" + + +@dataclass +class MethodSpec: + """Holds the raw LLM-generated JML comment block, preserved as-is.""" + + jml_block: str # raw JML comment block (//@ or /*@ ... @*/) from LLM code + auxiliaries: str = "" # helper predicates / model methods (prepended to stub) + + @property + def has_requires(self) -> bool: + return bool(re.search(r"requires\b", self.jml_block)) + + @property + def has_ensures(self) -> bool: + return bool(re.search(r"ensures\b", self.jml_block)) + + # Back-compat aliases (deprecated) + @property + def precondition(self) -> Optional[str]: + return self.jml_block if self.has_requires else None + + @property + def postcondition(self) -> Optional[str]: + return self.jml_block if self.has_ensures else None + + + +# JType — javalang-based type descriptor (from harness.py) + +@dataclass +class JType: + """ + Normalised Java type descriptor extracted from a javalang AST node. + + Examples + -------- + int → JType("int", array_dims=0) + int[] → JType("int", array_dims=1) + int[][] → JType("int", array_dims=2) + String → JType("String", array_dims=0) + List → JType("List", generic_args=["Integer"]) + Map> → JType("Map", generic_args=["String","List"]) + """ + + base: str + array_dims: int = 0 + generic_args: list = field(default_factory=list) + + PRIMITIVES = frozenset( + {"int", "long", "short", "byte", "double", "float", "boolean", "char"} + ) + COLLECTIONS = frozenset( + { + "List", + "ArrayList", + "LinkedList", + "Set", + "HashSet", + "TreeSet", + "Map", + "HashMap", + "TreeMap", + } + ) + + @property + def is_primitive(self) -> bool: + return self.base in self.PRIMITIVES + + @property + def is_array(self) -> bool: + return self.array_dims > 0 + + @property + def is_collection(self) -> bool: + return self.base in self.COLLECTIONS + + def java_decl(self) -> str: + """Full Java type declaration string, e.g. 'List' or 'int[][]'.""" + if self.generic_args: + args = ", ".join(self.generic_args) + base = f"{self.base}<{args}>" + else: + base = self.base + return base + "[]" * self.array_dims + + def element_type(self) -> "JType": + """Return the element type for array types (strip one dimension).""" + assert self.is_array, "element_type() called on non-array type" + return JType(self.base, self.array_dims - 1, self.generic_args) + + + +# Utility: parse a raw generic-arg string back to JType (from harness.py) + +def _split_generic_args(s: str) -> list[str]: + """Split 'String, List' respecting nested angle brackets.""" + depth, buf, result = 0, [], [] + for ch in s: + if ch == "<": + depth += 1 + buf.append(ch) + elif ch == ">": + depth -= 1 + buf.append(ch) + elif ch == "," and depth == 0: + result.append("".join(buf).strip()) + buf = [] + else: + buf.append(ch) + if buf: + result.append("".join(buf).strip()) + return result + + +def _parse_raw_jtype(raw: str) -> JType: + """ + Minimal parser for strings like "Integer", "int[]", "List", + "Map>". Used when rendering nested generics. + """ + raw = raw.strip() + array_dims = 0 + while raw.endswith("[]"): + array_dims += 1 + raw = raw[:-2] + m = re.match(r"^(\w+)<(.+)>$", raw) + if m: + base = m.group(1) + inner = _split_generic_args(m.group(2)) + return JType(base=base, array_dims=array_dims, generic_args=inner) + return JType(base=raw, array_dims=array_dims) + + + +# JavaMethodParser (from harness.py) + +class JavaMethodParser: + """ + Parses a Java source string (class or bare method) using javalang + and returns structured parameter / return type information. + """ + + def parse(self, source: str) -> dict: + wrapped, class_name = self._ensure_class(source) + try: + tree = javalang.parse.parse(wrapped) + except javalang.parser.JavaSyntaxError as e: + raise ValueError(f"javalang parse error: {e}") from e + + for _, node in tree: + if isinstance(node, jtree.MethodDeclaration): + return { + "class_name": class_name, + "method_name": node.name, + "return_type": self._jtype(node.return_type), + "params": [ + {"name": p.name, "jtype": self._jtype(p.type)} + for p in (node.parameters or []) + ], + } + raise ValueError("No MethodDeclaration found in the provided source.") + + @staticmethod + def _ensure_class(source: str) -> tuple[str, str]: + source = source.strip() + m = re.search(r"\bclass\s+(\w+)", source) + if m: + return source, m.group(1) + return f"class _Harness {{ {source} }}", "_Harness" + + def _jtype(self, node) -> JType: + if node is None: + return JType(base="void") + if isinstance(node, jtree.BasicType): + dims = len(node.dimensions) if node.dimensions else 0 + return JType(base=node.name, array_dims=dims) + if isinstance(node, jtree.ReferenceType): + dims = len(node.dimensions) if node.dimensions else 0 + generic_args = self._generic_args(node) + return JType(base=node.name, array_dims=dims, generic_args=generic_args) + return JType(base=str(node)) + + def _generic_args(self, node: jtree.ReferenceType) -> list[str]: + if not getattr(node, "arguments", None): + return [] + result = [] + for arg in node.arguments: + t = getattr(arg, "type", None) + if t is not None: + result.append(self._jtype(t).java_decl()) + elif hasattr(arg, "name"): + result.append(arg.name) + return result + + + +# JavaLiteralRenderer (from harness.py) + +class JavaLiteralRenderer: + """ + Converts a Python value to a syntactically valid Java literal / + initialiser expression, guided by a JType descriptor. + """ + + def render(self, jtype: JType, value: Any) -> str: + if value is None: + return "null" + if jtype.is_array: + return self._array(jtype, value) + if jtype.is_collection: + return self._collection(jtype, value) + return self._scalar(jtype.base, value) + + def _array(self, jtype: JType, value: Any) -> str: + elem_type = jtype.element_type() + if jtype.array_dims == 1: + elems = ", ".join(self._scalar(jtype.base, v) for v in value) + return f"new {jtype.base}[]{{{elems}}}" + rows = ", ".join(self._array(elem_type, row) for row in value) + inner = jtype.base + "[]" * (jtype.array_dims - 1) + return f"new {inner}[]{{{rows}}}" + + def _collection(self, jtype: JType, value: Any) -> str: + base = jtype.base + if base in ("Map", "HashMap", "TreeMap"): + return self._map(jtype, value) + if base in ("Set", "HashSet", "TreeSet"): + return self._set(jtype, value) + return self._list(jtype, value) + + def _list(self, jtype: JType, value: list) -> str: + elem = self._arg_type(jtype, 0) + elems = ", ".join(self.render(elem, v) for v in value) + concrete = "LinkedList" if jtype.base == "LinkedList" else "ArrayList" + return f"new java.util.{concrete}<>(java.util.Arrays.asList({elems}))" + + def _set(self, jtype: JType, value) -> str: + elem = self._arg_type(jtype, 0) + elems = ", ".join(self.render(elem, v) for v in value) + concrete = "TreeSet" if jtype.base == "TreeSet" else "HashSet" + return f"new java.util.{concrete}<>(java.util.Arrays.asList({elems}))" + + def _map(self, jtype: JType, value: dict) -> str: + k_type = self._arg_type(jtype, 0) + v_type = self._arg_type(jtype, 1) + concrete = "TreeMap" if jtype.base == "TreeMap" else "HashMap" + entries = "; ".join( + f"_m.put({self.render(k_type, k)}, {self.render(v_type, v)})" + for k, v in value.items() + ) + decl = jtype.java_decl() + return f"new java.util.{concrete}<{decl}>() {{{{ {entries}; }}}}" + + def _scalar(self, base: str, value: Any) -> str: + if base in ("int", "Integer", "short", "Short", "byte", "Byte"): + return str(int(value)) + if base in ("long", "Long"): + return f"{int(value)}L" + if base in ("double", "Double"): + return f"{float(value)}d" + if base in ("float", "Float"): + return f"{float(value)}f" + if base in ("boolean", "Boolean"): + return "true" if value else "false" + if base in ("char", "Character"): + return f"'{value}'" + if base == "String": + esc = str(value).replace("\\", "\\\\").replace('"', '\\"') + return f'"{esc}"' + return str(value) + + def _arg_type(self, jtype: JType, idx: int) -> JType: + if jtype.generic_args and idx < len(jtype.generic_args): + return _parse_raw_jtype(jtype.generic_args[idx]) + return JType(base="Object") + + + +# StubBuilder (from harness.py) + +class StubBuilder: + """ + Constructs Java harness stubs for each of the four Hoare triples. + """ + + def __init__(self): + self._renderer = JavaLiteralRenderer() + + def post_correctness_stub( + self, parsed: dict, spec: MethodSpec, pair: TestPair + ) -> str: + assumes = self._input_assumes(parsed, pair.inputs) + ret = self._return_stmt(parsed, pair.output) + return self._wrap_post(parsed, spec, assumes, ret) + + def post_completeness_stub( + self, parsed: dict, spec: MethodSpec, pair: TestPair, mutated_output: Any + ) -> str: + assumes = self._input_assumes(parsed, pair.inputs) + ret = self._return_stmt(parsed, mutated_output) + return self._wrap_post(parsed, spec, assumes, ret) + + def pre_correctness_stub( + self, + parsed: dict, + spec: MethodSpec, + case: InputCase, + original_source: str = "", + ) -> str: + if original_source: + return self._wrap_caller(parsed, spec, original_source, case.inputs) + assumes = self._input_assumes(parsed, case.inputs) + return self._wrap_pre(parsed, spec, assumes) + + def pre_completeness_stub( + self, + parsed: dict, + spec: MethodSpec, + case: InputCase, + original_source: str = "", + ) -> str: + if original_source: + return self._wrap_caller(parsed, spec, original_source, case.inputs) + assumes = self._input_assumes(parsed, case.inputs) + return self._wrap_pre(parsed, spec, assumes) + + def _input_assumes(self, parsed: dict, inputs: dict[str, Any]) -> str: + lines: list[str] = [] + for p in parsed["params"]: + val = inputs[p["name"]] + lines.extend(self._assume_for(p["name"], p["jtype"], val)) + return "\n".join(lines) + + def _assume_for(self, name: str, jtype: JType, value: Any) -> list[str]: + I = " " + if value is None: + return [f"{I}//@ assume {name} == null;"] + if jtype.is_array: + return self._assume_array(name, jtype, value) + if jtype.is_collection: + return self._assume_collection(name, jtype, value) + if jtype.base == "String": + lit = self._renderer._scalar("String", value) + return [f"{I}//@ assume {name} != null && {name}.equals({lit});"] + lit = self._renderer._scalar(jtype.base, value) + return [f"{I}//@ assume {name} == {lit};"] + + def _assume_array(self, name: str, jtype: JType, value: list) -> list[str]: + I = " " + lines = [ + f"{I}//@ assume {name} != null;", + f"{I}//@ assume {name}.length == {len(value)};", + ] + if jtype.array_dims == 1: + for i, v in enumerate(value): + lit = self._renderer._scalar(jtype.base, v) + lines.append(f"{I}//@ assume {name}[{i}] == {lit};") + elif jtype.array_dims >= 2: + elem = jtype.element_type() + for i, row in enumerate(value): + lines.append(f"{I}//@ assume {name}[{i}] != null;") + lines.append(f"{I}//@ assume {name}[{i}].length == {len(row)};") + if elem.array_dims == 0: + for j, v in enumerate(row): + lit = self._renderer._scalar(jtype.base, v) + lines.append(f"{I}//@ assume {name}[{i}][{j}] == {lit};") + return lines + + def _assume_collection( + self, name: str, jtype: JType, value: Any + ) -> list[str]: + I = " " + if value is None: + return [f"{I}//@ assume {name} == null;"] + lines = [f"{I}//@ assume {name} != null;"] + if isinstance(value, dict): + lines.append(f"{I}//@ assume {name}.size() == {len(value)};") + elif isinstance(value, (list, set)): + lines.append(f"{I}//@ assume {name}.size() == {len(value)};") + return lines + + def _return_stmt(self, parsed: dict, value: Any) -> str: + rt = parsed["return_type"] + lit = self._renderer.render(rt, value) + return f" return {lit};" + + def _wrap_post( + self, parsed: dict, spec: MethodSpec, assumes: str, ret_stmt: str + ) -> str: + params_decl = ", ".join( + f"{p['jtype'].java_decl()} {p['name']}" for p in parsed["params"] + ) + ret = parsed["return_type"].java_decl() + mname = parsed["method_name"] + cname = parsed["class_name"] + aux = spec.auxiliaries or "" + jml = self._indent_jml(spec.jml_block, " ") + return ( + f"{aux}\n" + f"//@ nullable_by_default\n" + f"public class {cname}Harness {{\n" + f"{jml}\n" + f" public static {ret} {mname}({params_decl}) {{\n" + f"{assumes}\n" + f"{ret_stmt}\n" + f" }}\n" + f"}}\n" + ) + + def _wrap_pre(self, parsed: dict, spec: MethodSpec, assumes: str) -> str: + params_decl = ", ".join( + f"{p['jtype'].java_decl()} {p['name']}" for p in parsed["params"] + ) + mname = parsed["method_name"] + cname = parsed["class_name"] + aux = spec.auxiliaries or "" + jml = self._indent_jml(spec.jml_block, " ") + return ( + f"{aux}\n" + f"//@ nullable_by_default\n" + f"public class {cname}Harness {{\n" + f"{jml}\n" + f" public static void {mname}({params_decl}) {{\n" + f"{assumes}\n" + f" }}\n" + f"}}\n" + ) + + def _wrap_caller( + self, + parsed: dict, + spec: MethodSpec, + original_source: str, + inputs: dict[str, Any], + ) -> str: + mname = parsed["method_name"] + cname = parsed["class_name"] + call_args = ", ".join( + self._renderer.render(p["jtype"], inputs[p["name"]]) + for p in parsed["params"] + ) + src = re.sub(r"\bpublic\s+class\b", "class", original_source, count=1) + return ( + f"//@ nullable_by_default\n" + f"{src}\n\n" + f"public class {cname}Harness {{\n" + f" public static void check() {{\n" + f" {cname}.{mname}({call_args});\n" + f" }}\n" + f"}}\n" + ) + + @staticmethod + def _indent_jml(jml_block: str, indent: str) -> str: + return "\n".join( + indent + line.strip() + for line in jml_block.splitlines() + if line.strip() + ) + + + +# OutputMutator (from harness.py) + +class OutputMutator: + """ + Generates up to k output mutants for PostCompleteness. + """ + + def __init__(self, k: int = 5): + self.k = k + + def mutate(self, jtype: JType, value: Any) -> list[Any]: + if jtype.is_array: + return self._mutate_array(list(value) if value else []) + if jtype.is_collection: + return self._mutate_collection(jtype, value) + return self._mutate_scalar(jtype.base, value) + + def _mutate_scalar(self, base: str, v: Any) -> list: + if base in ("int", "long", "short", "byte", "Integer", "Long"): + v = int(v) + return list(dict.fromkeys([v + 1, v - 1, v + 2, v - 2, 0]))[: self.k] + if base in ("double", "float", "Double", "Float"): + v = float(v) + return [v + 1.0, v - 1.0, v * 2.0, -v][: self.k] + if base in ("boolean", "Boolean"): + return [not v] + if base == "String": + return [v + "_x", (v[:-1] if v else "x"), v.upper(), "", v[::-1]][: self.k] + if base in ("char", "Character"): + c = ord(v) + return [chr(c + 1), chr(c - 1)][: self.k] + return [] + + def _mutate_array(self, v: list) -> list: + mutants: list = [] + if v: + mutants.append(v[:-1]) + last = v[-1] + if not isinstance(last, list): + mutants.append(v + [last + 1]) + if all(not isinstance(x, list) for x in v): + mutants.append([x + 1 for x in v]) + mutants.append([]) + return [m for m in mutants if m != v][: self.k] + + def _mutate_collection(self, jtype: JType, v: Any) -> list: + if jtype.base in ("Map", "HashMap", "TreeMap"): + d = dict(v) if v else {} + mutants: list = [] + if d: + k0 = next(iter(d)) + mutants.append({k: val for k, val in d.items() if k != k0}) + mutants.append({}) + return mutants[: self.k] + return self._mutate_array(list(v) if v else []) + + + +# eval_spec helpers (from eval_spec.py) + +def _find_method_line(source: str) -> int | None: + lines = source.splitlines() + leading_blanks = 0 + for line in lines: + if line.strip(): + break + leading_blanks += 1 + + stripped = source.strip() + has_class = bool(re.search(r"\bclass\s+\w+", stripped)) + if has_class: + to_parse = stripped + offset = leading_blanks + else: + to_parse = f"class _Wrapper {{\n{stripped}\n}}" + offset = leading_blanks - 1 + + try: + tree = javalang.parse.parse(to_parse) + except javalang.parser.JavaSyntaxError: + return None + + for _, node in tree: + if isinstance(node, jtree.MethodDeclaration) and node.position: + return node.position.line + offset + return None + + +def extract_jml_spec(source: str) -> MethodSpec: + """ + Extract the raw JML comment block from above the method declaration. + """ + lines = source.splitlines() + method_line = _find_method_line(source) + + if method_line is not None: + end = method_line - 2 + while end >= 0: + s = lines[end].strip() + if ( + s.startswith("//@") + or s.startswith("/*@") + or s.endswith("@*/") + or s.endswith("*/") + ): + break + if not s or s.startswith("@"): + end -= 1 + else: + break + + start = end + in_block_comment = False + while start >= 0: + s = lines[start].strip() + if s.endswith("@*/") or s.endswith("*/"): + in_block_comment = True + if in_block_comment: + if s.startswith("/*@") or s.startswith("/*"): + in_block_comment = False + start -= 1 + continue + if s.startswith("//@"): + start -= 1 + continue + break + jml_block = "\n".join(lines[start + 1 : end + 1]) + else: + jml_lines = [ + l + for l in lines + if l.strip().startswith("//@") or l.strip().startswith("/*@") + ] + jml_block = "\n".join(jml_lines) + + return MethodSpec(jml_block=jml_block) + + +@dataclass +class ReadOp: + """One input-reading operation derived from Test.java.""" + + name: str + jtype: JType + mode: str # scalar | grouped_scalar | string | array_direct | array_sized | + # array_2d | array_2d_rc | map | set | list_direct + group_idx: int = -1 + + +def _walk_ast(node): + if node is None or not isinstance(node, jtree.Node): + return + yield node + for attr_name in node.attrs: + child = getattr(node, attr_name, None) + if child is None: + continue + if isinstance(child, jtree.Node): + yield from _walk_ast(child) + elif isinstance(child, (list, tuple)): + for item in child: + if isinstance(item, jtree.Node): + yield from _walk_ast(item) + + +def _is_string_array_decl(type_node, declarator) -> bool: + if not isinstance(type_node, jtree.ReferenceType): + return False + if type_node.name != "String": + return False + if type_node.dimensions and len(type_node.dimensions) > 0: + return True + if declarator.dimensions and len(declarator.dimensions) > 0: + return True + return False + + +def _ast_has_method_call(node, method_name: str) -> bool: + for n in _walk_ast(node): + if isinstance(n, jtree.MethodInvocation) and n.member == method_name: + return True + return False + + +def _ast_find_member_ref(node) -> str | None: + for n in _walk_ast(node): + if isinstance(n, jtree.MemberReference) and not n.selectors: + return n.member + return None + + +def _ast_find_array_access(node) -> tuple[str, int] | None: + for n in _walk_ast(node): + if isinstance(n, jtree.MemberReference) and n.selectors: + for sel in n.selectors: + if isinstance(sel, jtree.ArraySelector): + idx_node = sel.index + if isinstance(idx_node, jtree.Literal): + try: + return (n.member, int(idx_node.value)) + except (ValueError, TypeError): + pass + return None + + +def _javalang_detect( + test_src: str, all_param_names: set[str], params: list[dict] +) -> tuple[dict[str, int], bool, bool, dict[str, str]]: + grouped_indices: dict[str, int] = {} + has_2d_rc = False + has_sized_1d = False + input_order_map: dict[str, str] = {} + + parseable = re.sub(r"\bvar\s+(\w+)\s*=", r"Object \1 =", test_src) + tree = javalang.parse.parse(parseable) + + main_body = None + for _, node in tree: + if isinstance(node, jtree.MethodDeclaration) and node.name == "main": + main_body = node.body + break + if not main_body: + return grouped_indices, has_2d_rc, has_sized_1d, input_order_map + + split_vars: set[str] = set() + rc_vars: set[str] = set() + + for stmt in main_body: + if not isinstance(stmt, jtree.LocalVariableDeclaration): + continue + for decl in stmt.declarators: + vname = decl.name + init = decl.initializer + + if ( + _is_string_array_decl(stmt.type, decl) + and init is not None + and _ast_has_method_call(init, "split") + ): + split_vars.add(vname) + if vname.startswith(("_rc", "rc")): + rc_vars.add(vname) + has_2d_rc = True + continue + + if vname in all_param_names and init is not None: + arr_access = _ast_find_array_access(init) + if arr_access is not None: + arr_name, idx = arr_access + if arr_name in split_vars and arr_name not in rc_vars: + grouped_indices[vname] = idx + + non_rc_splits = split_vars - rc_vars + check_inline = bool(non_rc_splits) and not grouped_indices + for stmt in main_body: + for n in _walk_ast(stmt): + if not ( + isinstance(n, jtree.MethodInvocation) + and n.member == "solve" + and n.arguments + ): + continue + for arg_idx, arg in enumerate(n.arguments): + if arg_idx >= len(params): + break + sol_name = params[arg_idx]["name"] + + if check_inline: + arr_access = _ast_find_array_access(arg) + if arr_access is not None and arr_access[0] in non_rc_splits: + grouped_indices[sol_name] = arr_access[1] + + ref = _ast_find_member_ref(arg) + if ref is not None and ref in all_param_names: + input_order_map[sol_name] = ref + + return grouped_indices, has_2d_rc, has_sized_1d, input_order_map + + +def _is_nested_collection(inner_type_str: str) -> bool: + return inner_type_str.startswith( + ("List", "ArrayList", "LinkedList") + ) or inner_type_str.endswith("[]") + + +def _leaf_element_type(jtype: JType) -> str: + if jtype.is_array: + return jtype.base + if jtype.is_collection and jtype.generic_args: + inner = jtype.generic_args[0] + m = re.match(r"^(\w+)<(.+)>$", inner) + if m: + inner_base = m.group(1) + if inner_base in ( + "List", + "ArrayList", + "LinkedList", + "Set", + "HashSet", + "TreeSet", + ): + return m.group(2).strip() + return inner + if inner.endswith("[]"): + return inner[:-2] + return inner + return jtype.base + + +def _regex_fallback( + test_src: str, all_param_names: set[str] +) -> tuple[dict[str, int], bool, bool]: + grouped_indices: dict[str, int] = {} + + split_var_names = re.findall( + r"String\[\]\s+(\w+)\s*=\s*scanner\." + r"(?:hasNextLine\s*\(\)\s*\?\s*)?nextLine\(\).*?split\s*\(", + test_src, + ) + for sv in split_var_names: + if re.match(r"_?rc|_?pr|_raw_", sv): + continue + for m in re.finditer( + rf"(\w+)\s*=\s*\w+\.parse\w+\(\s*{re.escape(sv)}" + rf"\s*\[\s*(\d+)\s*\]\s*\)", + test_src, + ): + grouped_indices[m.group(1)] = int(m.group(2)) + for m in re.finditer( + rf"(\w+)\s*=\s*{re.escape(sv)}" + rf"\s*\[\s*(\d+)\s*\]\.charAt\s*\(\s*0\s*\)", + test_src, + ): + grouped_indices[m.group(1)] = int(m.group(2)) + for m in re.finditer( + rf"(?:String\s+)?(\w+)\s*=\s*{re.escape(sv)}" rf"\s*\[\s*(\d+)\s*\]\s*;", + test_src, + ): + if m.group(1) in all_param_names: + grouped_indices[m.group(1)] = int(m.group(2)) + + has_2d_rc = bool( + re.search( + r"_?rc[\w]*\s*=\s*scanner\." r"(?:hasNextLine\s*\(\)\s*\?\s*)?nextLine", + test_src, + ) + ) + has_sized_1d = bool( + re.search(r"int\s+n\d+\s*=\s*Integer\.parseInt\(scanner\.nextLine", test_src) + ) + + return grouped_indices, has_2d_rc, has_sized_1d + + +def detect_input_format(test_src: str, params: list[dict]) -> list[ReadOp]: + """ + Analyse machine-generated Test.java to decide how each parameter is + read from stdin. + """ + ops: list[ReadOp] = [] + + param_names = {p["name"] for p in params} + positional_names = {f"p{i}" for i in range(len(params))} + all_param_names = param_names | positional_names + + input_order_map: dict[str, str] = {} + try: + grouped_indices, has_2d_rc, has_sized_1d, input_order_map = _javalang_detect( + test_src, all_param_names, params + ) + except Exception: + grouped_indices, has_2d_rc, has_sized_1d = _regex_fallback( + test_src, all_param_names + ) + + ordered_params = list(params) + if input_order_map: + pn_to_sol: dict[str, dict] = {} + for sol_name, pn_name in input_order_map.items(): + for p in params: + if p["name"] == sol_name: + pn_to_sol[pn_name] = p + break + if len(pn_to_sol) == len(params): + ordered_params = [ + pn_to_sol[f"p{i}"] for i in range(len(params)) if f"p{i}" in pn_to_sol + ] + if len(ordered_params) != len(params): + ordered_params = list(params) + + for pi, p in enumerate(ordered_params): + jtype = p["jtype"] + name = p["name"] + tvar = f"p{pi}" + + if jtype.base in ("HashMap", "Map", "TreeMap"): + ops.append(ReadOp(name, jtype, "map")) + continue + if jtype.base in ("HashSet", "Set", "TreeSet"): + ops.append(ReadOp(name, jtype, "set")) + continue + if jtype.base in ("List", "ArrayList", "LinkedList"): + if jtype.generic_args and _is_nested_collection(jtype.generic_args[0]): + mode = "array_2d_rc" if has_2d_rc else "array_2d" + ops.append(ReadOp(name, jtype, mode)) + else: + ops.append(ReadOp(name, jtype, "list_direct")) + continue + if jtype.is_array and jtype.array_dims >= 2: + mode = "array_2d_rc" if has_2d_rc else "array_2d" + ops.append(ReadOp(name, jtype, mode)) + continue + if jtype.is_array: + mode = "array_sized" if has_sized_1d else "array_direct" + ops.append(ReadOp(name, jtype, mode)) + continue + if jtype.base == "String": + ops.append(ReadOp(name, jtype, "string")) + continue + + gidx = grouped_indices.get(name, grouped_indices.get(tvar, -1)) + if gidx >= 0: + ops.append(ReadOp(name, jtype, "grouped_scalar", group_idx=gidx)) + else: + ops.append(ReadOp(name, jtype, "scalar")) + + return ops + + +def _parse_scalar(type_name: str, s: str) -> Any: + s = s.strip() + if type_name in ("int", "Integer", "short", "Short", "byte", "Byte"): + return int(s) + if type_name in ("long", "Long"): + return int(s) + if type_name in ("double", "Double"): + return float(s) + if type_name in ("float", "Float"): + return float(s) + if type_name in ("boolean", "Boolean"): + return s.lower() == "true" + if type_name in ("char", "Character"): + return s + return s + + +def parse_input(input_str: str, ops: list[ReadOp]) -> dict[str, Any]: + lines = input_str.split("\n") + pos = 0 + result: dict[str, Any] = {} + + i = 0 + while i < len(ops): + op = ops[i] + + if op.mode == "grouped_scalar": + parts = lines[pos].strip().split() + pos += 1 + j = i + while j < len(ops) and ops[j].mode == "grouped_scalar": + g = ops[j] + result[g.name] = _parse_scalar(g.jtype.base, parts[g.group_idx]) + j += 1 + i = j + continue + + if op.mode == "scalar": + result[op.name] = _parse_scalar(op.jtype.base, lines[pos].strip()) + pos += 1 + elif op.mode == "string": + result[op.name] = lines[pos] + pos += 1 + elif op.mode == "array_direct": + parts = lines[pos].strip().split() + result[op.name] = [_parse_scalar(op.jtype.base, p) for p in parts] + pos += 1 + elif op.mode == "array_sized": + n = int(lines[pos].strip()) + pos += 1 + if n > 0: + parts = lines[pos].strip().split() + result[op.name] = [_parse_scalar(op.jtype.base, p) for p in parts] + pos += 1 + else: + result[op.name] = [] + elif op.mode == "array_2d": + elem = _leaf_element_type(op.jtype) + n_rows = int(lines[pos].strip()) + pos += 1 + mat = [] + for _ in range(n_rows): + if pos < len(lines) and lines[pos].strip(): + row = [_parse_scalar(elem, x) for x in lines[pos].strip().split()] + mat.append(row) + pos += 1 + else: + mat.append([]) + result[op.name] = mat + elif op.mode == "array_2d_rc": + elem = _leaf_element_type(op.jtype) + rc = lines[pos].strip().split() + n_rows, n_cols = int(rc[0]), int(rc[1]) + pos += 1 + mat = [] + if n_cols == 0: + mat = [[] for _ in range(n_rows)] + else: + for _ in range(n_rows): + if pos < len(lines): + row = [ + _parse_scalar(elem, x) for x in lines[pos].strip().split() + ] + mat.append(row) + pos += 1 + else: + mat.append([]) + result[op.name] = mat + elif op.mode == "map": + n = int(lines[pos].strip()) + pos += 1 + d: dict = {} + ktype = op.jtype.generic_args[0] if op.jtype.generic_args else "String" + vtype = ( + op.jtype.generic_args[1] + if len(op.jtype.generic_args) > 1 + else "Integer" + ) + for _ in range(n): + parts = lines[pos].split("\t") + d[_parse_scalar(ktype, parts[0])] = _parse_scalar( + vtype, parts[1].strip() + ) + pos += 1 + result[op.name] = d + elif op.mode == "set": + n = int(lines[pos].strip()) + pos += 1 + etype = op.jtype.generic_args[0] if op.jtype.generic_args else "Integer" + parts = lines[pos].strip().split() + result[op.name] = [_parse_scalar(etype, p) for p in parts] + pos += 1 + elif op.mode == "list_direct": + etype = op.jtype.generic_args[0] if op.jtype.generic_args else "Integer" + line = lines[pos].strip() + if line: + parts = line.split() + result[op.name] = [_parse_scalar(etype, p) for p in parts] + else: + result[op.name] = [] + pos += 1 + + i += 1 + + return result + + +def parse_output(output_str: str, return_type: JType) -> Any: + output_str = output_str.rstrip("\n") + + if return_type.base == "void": + return None + + if return_type.base in ("HashMap", "Map", "TreeMap"): + lines = output_str.split("\n") + count = int(lines[0].strip()) + ktype = return_type.generic_args[0] if return_type.generic_args else "String" + vtype = ( + return_type.generic_args[1] + if len(return_type.generic_args) > 1 + else "Integer" + ) + d: dict = {} + for j in range(1, count + 1): + parts = lines[j].split("\t") + d[_parse_scalar(ktype, parts[0])] = _parse_scalar(vtype, parts[1].strip()) + return d + + if return_type.is_array and return_type.array_dims >= 2: + rows = [] + for line in output_str.split("\n"): + line = line.strip() + if line: + row = [_parse_scalar(return_type.base, x) for x in line.split()] + rows.append(row) + return rows + + if return_type.is_array: + tokens = output_str.strip().split() + if not tokens or tokens == [""]: + return [] + return [_parse_scalar(return_type.base, t) for t in tokens] + + if return_type.base in ("List", "ArrayList", "LinkedList"): + tokens = output_str.strip().split() + etype = return_type.generic_args[0] if return_type.generic_args else "Integer" + if not tokens or tokens == [""]: + return [] + return [_parse_scalar(etype, t) for t in tokens] + + if return_type.base in ("Set", "HashSet", "TreeSet"): + tokens = output_str.strip().split() + etype = return_type.generic_args[0] if return_type.generic_args else "Integer" + if not tokens or tokens == [""]: + return [] + return [_parse_scalar(etype, t) for t in tokens] + + return _parse_scalar(return_type.base, output_str.strip()) + + +def generate_invalid_inputs( + params: list[dict], valid_inputs: list[dict[str, Any]] +) -> list[InputCase]: + """ + Auto-generate boundary / invalid input cases (T-) for PreCompleteness. + """ + if not valid_inputs: + return [] + + base = dict(valid_inputs[0]) + invalid: list[InputCase] = [] + + for p in params: + jtype = p["jtype"] + name = p["name"] + + is_ref = not jtype.is_primitive or jtype.is_array or jtype.is_collection + if is_ref: + case = dict(base) + case[name] = None + invalid.append(InputCase(case, False, f"null_{name}")) + + if jtype.is_array or jtype.is_collection: + case = dict(base) + case[name] = {} if jtype.base in ("HashMap", "Map", "TreeMap") else [] + invalid.append(InputCase(case, False, f"empty_{name}")) + + if ( + jtype.is_array + and isinstance(base.get(name), list) + and len(base.get(name, [])) > 1 + ): + case = dict(base) + case[name] = [base[name][0]] + invalid.append(InputCase(case, False, f"single_{name}")) + + if ( + not jtype.is_array + and not jtype.is_collection + and jtype.base + in ("int", "Integer", "long", "Long", "short", "Short", "byte", "Byte") + ): + case = dict(base) + case[name] = -1 + invalid.append(InputCase(case, False, f"neg_{name}")) + + return invalid + + + +# Task / TestCase data classes (from eval_llm_response.py) + +@dataclass +class TestCase: + input: str + output: str + + @classmethod + def from_dict(cls, data: dict[str, str]) -> "TestCase": + return cls(input=data["input"], output=data["output"]) + + +@dataclass +class Task: + task_id: str + code: str + class_name: str + test_name: str + javadoc: str + category: str + origin_id: str + test_code: str = "" + test_inputs: list[TestCase] = field(default_factory=list) + generated_test_cases: list[TestCase] = field(default_factory=list) + + @classmethod + def from_dict(cls, data: dict[str, Any]) -> "Task": + return cls( + task_id=data["task_id"], + code=data["code"], + class_name=data["class_name"], + test_name=data["test_name"], + javadoc=data.get("javadoc", ""), + category=data.get("category", ""), + origin_id=data.get("origin_id", ""), + test_code=data.get("test_code", ""), + test_inputs=[TestCase.from_dict(tc) for tc in data.get("test_inputs", [])], + generated_test_cases=[ + TestCase.from_dict(tc) + for tc in data.get("generated_test_cases", []) + ], + ) + + + +# OpenJMLRunnerPersistent (from eval_llm_response.py) + +class OpenJMLRunnerPersistent: + """Runs OpenJML ESC, writing harness stubs to an actual directory.""" + + def __init__(self, openjml_path: str, output_dir: str, timeout: int = 300): + self.openjml_path = openjml_path + self.output_dir = output_dir + self.timeout = timeout + os.makedirs(output_dir, exist_ok=True) + + def verify( + self, java_source: str, class_name: str, label: str = "" + ) -> tuple[VerifyResult, str]: + harness_class = f"{class_name}Harness" + fname = f"{harness_class}.java" + if label: + safe_label = re.sub(r"[^\w\-]", "_", label) + sub_dir = os.path.join(self.output_dir, safe_label) + os.makedirs(sub_dir, exist_ok=True) + path = os.path.join(sub_dir, fname) + else: + path = os.path.join(self.output_dir, fname) + with open(path, "w") as f: + f.write(java_source) + cmd = [ + "openjml", + "--esc", + "--esc-max-warnings", + "1", + "--prover=cvc4", + "--nonnull-by-default", + "--arithmetic-failure=quiet", + "-nowarn", + path, + ] + proc = subprocess.Popen( + cmd, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + text=True, + preexec_fn=os.setsid, + ) + try: + stdout, stderr = proc.communicate(timeout=self.timeout) + out = stdout + stderr + return self._parse(proc.returncode, out), out + except subprocess.TimeoutExpired: + return VerifyResult.UNKNOWN, "timeout" + except FileNotFoundError: + raise RuntimeError(f"OpenJML binary not found at '{self.openjml_path}'.") + except Exception as e: + return VerifyResult.UNKNOWN, f"Error: {str(e)}" + finally: + try: + os.killpg(os.getpgid(proc.pid), signal.SIGKILL) + except ProcessLookupError: + pass + + @staticmethod + def _parse(returncode: int, output: str) -> VerifyResult: + low = output.strip().lower() + if re.search(r"[1-9]\d* warning", low): + return VerifyResult.FAIL + if re.search(r"[1-9]\d* verification failure", low): + return VerifyResult.FAIL + if re.search(r"\berror\b", low): + return VerifyResult.FAIL + if returncode == 0 or "verified" in low or "0 warnings" in low or low == "": + return VerifyResult.OK + return VerifyResult.UNKNOWN + + + +# PairResult (from eval_llm_response.py) + +@dataclass +class PairResult: + """All 4 metric results for a single test pair.""" + + pair_idx: int + post_correct_detail: dict = field(default_factory=dict) + post_complete_details: list[dict] = field(default_factory=list) + pre_correct_detail: dict = field(default_factory=dict) + pre_complete_details: list[dict] = field(default_factory=list) + + + +# Inner thread helper (from eval_llm_response.py) + +def _log( + verbose: bool, + task_id: str, + metric: str, + label: str, + verdict: VerifyResult, + desired: bool, + extra: str = "", +) -> None: + if not verbose: + return + status = "pass" if desired else "fail" + ex = f" [{extra}]" if extra else "" + logger.debug(f"[{task_id}] [{metric}] {label}{ex} {verdict.value} {status}") + + +def _evaluate_one_pair( + pair_idx: int, + pair: TestPair, + valid_input_case: InputCase, + invalid_cases: list[InputCase], + parsed: dict, + spec: MethodSpec, + rtype: JType, + builder: StubBuilder, + mutator: OutputMutator, + runner: OpenJMLRunnerPersistent, + cname: str, + verbose: bool, + task_id: str, + java_source: str = "", +) -> PairResult: + """Compute all 4 metrics for a single test pair in its own thread.""" + result = PairResult(pair_idx=pair_idx) + + # PostCorrectness + if spec.postcondition is not None: + stub = builder.post_correctness_stub(parsed, spec, pair) + verdict, _ = runner.verify(stub, cname, f"post_correct_{pair.label}") + ok = verdict == VerifyResult.OK + result.post_correct_detail = { + "label": pair.label, + "verdict": verdict.value, + "pass": ok, + "stub": stub, + } + _log(verbose, task_id, "PostCorrectness", pair.label, verdict, ok) + + # PostCompleteness + if spec.postcondition is not None: + for mut_out in mutator.mutate(rtype, pair.output): + stub = builder.post_completeness_stub(parsed, spec, pair, mut_out) + lbl = f"post_complete_{pair.label}_{str(mut_out)[:20]}" + verdict, _ = runner.verify(stub, cname, lbl) + killed = verdict == VerifyResult.FAIL + result.post_complete_details.append( + { + "label": pair.label, + "mutant": str(mut_out), + "verdict": verdict.value, + "killed": killed, + "stub": stub, + } + ) + _log( + verbose, + task_id, + "PostCompleteness", + pair.label, + verdict, + killed, + f"mutant={mut_out}", + ) + + # PreCorrectness + if spec.precondition is not None: + stub = builder.pre_correctness_stub( + parsed, spec, valid_input_case, original_source=java_source + ) + verdict, _ = runner.verify( + stub, cname, f"pre_correct_{valid_input_case.label}" + ) + ok = verdict == VerifyResult.OK + result.pre_correct_detail = { + "label": valid_input_case.label, + "verdict": verdict.value, + "pass": ok, + "stub": stub, + } + _log(verbose, task_id, "PreCorrectness", valid_input_case.label, verdict, ok) + + # PreCompleteness + if spec.precondition is not None: + for case in invalid_cases: + stub = builder.pre_completeness_stub( + parsed, spec, case, original_source=java_source + ) + verdict, _ = runner.verify(stub, cname, f"pre_complete_{case.label}") + rejected = verdict == VerifyResult.FAIL + result.pre_complete_details.append( + { + "label": case.label, + "verdict": verdict.value, + "rejected": rejected, + "stub": stub, + } + ) + _log(verbose, task_id, "PreCompleteness", case.label, verdict, rejected) + + return result + + + +# Main evaluation entry point + +def evaluate_problem( + task: Task, + llm_code: str, + openjml_path: str = "openjml", + output_dir: str = "veriact_outputs", + verbose: bool = False, + max_pairs: int = 5, + run_id: str = "", +) -> dict: + """ + Evaluate one task against LLM-generated JML annotations. + + Each test pair gets its own thread to compute all 4 metrics in parallel: + - PostCorrectness + - PostCompleteness + - PreCorrectness + - PreCompleteness + + Parameters + ---------- + task : Task object with benchmark Solution.java, Test.java, and IO pairs + llm_code : LLM-generated Java source with JML annotations + openjml_path : path to the OpenJML binary (default: "openjml") + output_dir : directory to store harness stub files + verbose : print per-case verdicts + max_pairs : max test pairs to use (0 = all) + + Returns + ------- + dict with keys: task_id, post_correctness, post_completeness, + pre_correctness, pre_completeness + Each metric value is a dict: {score, passed, total, details} + """ + solution_src = task.code + test_src = task.test_code + io_pairs = [{"input": tc.input, "output": tc.output} for tc in task.test_inputs] + io_pairs_gen = [ + {"input": tc.input, "output": tc.output} for tc in task.generated_test_cases + ] + + if max_pairs > 0: + io_pairs = io_pairs[:max_pairs] + remaining = max_pairs - len(io_pairs) + if remaining > 0: + io_pairs.extend(io_pairs_gen[:remaining]) + + # parse method signature from benchmark Solution.java + parser = JavaMethodParser() + bench_parsed = parser.parse(solution_src) + bench_params = bench_parsed["params"] + return_type = bench_parsed["return_type"] + + # extract JML spec from LLM code + spec = extract_jml_spec(llm_code) + if spec.postcondition is None: + logger.warning(f"[{task.task_id}] no JML ensures found") + + # parse LLM method signature + try: + llm_parsed = parser.parse(llm_code) + llm_params = llm_parsed["params"] + except (ValueError, Exception): + llm_parsed = bench_parsed + llm_params = bench_params + + # detect input format from Test.java + read_ops = detect_input_format(test_src, bench_params) + + # parse io_pairs into TestPair / InputCase objects + test_pairs: list[TestPair] = [] + valid_inputs: list[dict] = [] + + for idx, pair in enumerate(io_pairs): + try: + inputs_bench = parse_input(pair["input"], read_ops) + output = parse_output(pair["output"], return_type) + except Exception as e: + if verbose: + logger.warning(f"[{task.task_id}] skipping case {idx}: {e}") + continue + + inputs_llm: dict[str, Any] = {} + for bp, lp in zip(bench_params, llm_params): + inputs_llm[lp["name"]] = inputs_bench[bp["name"]] + + test_pairs.append(TestPair(inputs_llm, output, f"case_{idx}")) + valid_inputs.append(inputs_llm) + + if not test_pairs: + logger.error(f"[{task.task_id}] no test pairs could be parsed") + return {} + + # build InputCases for Pre metrics + valid_input_cases = [InputCase(tp.inputs, True, tp.label) for tp in test_pairs] + invalid_input_cases = generate_invalid_inputs(llm_params, valid_inputs) + + # setup + builder = StubBuilder() + mutator = OutputMutator(k=5) + parsed = llm_parsed + cname = parsed["class_name"] + rtype = parsed["return_type"] + + safe_task_id = task.task_id.replace("/", "_").replace("\\", "_") + if run_id: + stubs_dir = os.path.join(output_dir, "stubs", safe_task_id, run_id) + else: + stubs_dir = os.path.join(output_dir, "stubs", safe_task_id) + runner = OpenJMLRunnerPersistent(openjml_path, stubs_dir) + + # distribute invalid cases round-robin across test pairs + invalid_per_pair: list[list[InputCase]] = [[] for _ in test_pairs] + for i, ic in enumerate(invalid_input_cases): + invalid_per_pair[i % len(test_pairs)].append(ic) + + # launch one thread per test pair + n_threads = len(test_pairs) + pair_results: list[PairResult] = [None] * n_threads # type: ignore + + with ThreadPoolExecutor(max_workers=n_threads) as pool: + future_to_idx = { + pool.submit( + _evaluate_one_pair, + idx, + pair, + valid_input_cases[idx], + invalid_per_pair[idx], + parsed, + spec, + rtype, + builder, + mutator, + runner, + cname, + verbose, + task.task_id, + llm_code, + ): idx + for idx, pair in enumerate(test_pairs) + } + for future in as_completed(future_to_idx): + idx = future_to_idx[future] + try: + pair_results[idx] = future.result() + except Exception as e: + logger.error(f"[{task.task_id}] pair {idx}: {e}") + + # aggregate PairResults into HarnessResults + pc_details: list[dict] = [] + pcl_details: list[dict] = [] + prc_details: list[dict] = [] + prl_details: list[dict] = [] + + for pr in pair_results: + if pr is None: + continue + if pr.post_correct_detail: + pc_details.append(pr.post_correct_detail) + pcl_details.extend(pr.post_complete_details) + if pr.pre_correct_detail: + prc_details.append(pr.pre_correct_detail) + prl_details.extend(pr.pre_complete_details) + + results: dict[str, HarnessResult] = {} + + hr = HarnessResult("PostCorrectness", len(pc_details), 0) + hr.passed = sum(1 for d in pc_details if d.get("pass")) + hr.details = pc_details + results["post_correctness"] = hr + + hr = HarnessResult("PostCompleteness", len(pcl_details), 0) + hr.passed = sum(1 for d in pcl_details if d.get("killed")) + hr.details = pcl_details + results["post_completeness"] = hr + + hr = HarnessResult("PreCorrectness", len(prc_details), 0) + hr.passed = sum(1 for d in prc_details if d.get("pass")) + hr.details = prc_details + results["pre_correctness"] = hr + + hr = HarnessResult("PreCompleteness", len(prl_details), 0) + hr.passed = sum(1 for d in prl_details if d.get("rejected")) + hr.details = prl_details + results["pre_completeness"] = hr + + # summary + summary_lines = [f"Spec-Harness | task: {task.task_id} | method: {parsed['method_name']}"] + for r in results.values(): + summary_lines.append(f" {r}") + logger.info("\n".join(summary_lines)) + + # build output dict + return { + "task_id": task.task_id, + "post_correctness": results["post_correctness"].score, + "post_completeness": results["post_completeness"].score, + "pre_correctness": results["pre_correctness"].score, + "pre_completeness": results["pre_completeness"].score, + } diff --git a/agent_harness/templates/requirements.txt b/agent_harness/templates/requirements.txt new file mode 100644 index 0000000..a50e7ff --- /dev/null +++ b/agent_harness/templates/requirements.txt @@ -0,0 +1 @@ +javalang>=0.13.0 diff --git a/agent_harness/templates/root_README.md.tmpl b/agent_harness/templates/root_README.md.tmpl new file mode 100644 index 0000000..6b59eb9 --- /dev/null +++ b/agent_harness/templates/root_README.md.tmpl @@ -0,0 +1,74 @@ +# Agent comparison root — {{BENCHMARK}} ({{N_TASKS}} tasks, {{MODE}}) + +Self-contained working dirs (one per task) plus a driver and aggregator, for +running and comparing coding agents on JML-spec synthesis. Each task dir holds the +problem (`Solution.java`, `Test.java`, `tests/`) and the four tools as shell +scripts (`verify.sh`, `run_specharness.sh`, `submit.sh`). The agent edits +`Solution.java`, iterates verify → fix → score, then submits. `verify.sh` runs +OpenJML and includes the error analysis (failure modes + repair hints) in its +output. + +## Layout + +``` +. +├── run_agents.py # fan out one fresh agent session per task dir +├── collect.py # aggregate every submission.json -> comparison.{json,csv} +├── README.md +└── / # one self-contained dir per task + ├── Solution.java # agent edits this (add JML; class stays `Solution`) + ├── Test.java + ├── tests/case_*.json + ├── AGENTS.md # the prompt/instructions for the agent + ├── verify.sh run_specharness.sh submit.sh + └── harness/ # vendored CLI + tools (+ task.json, .venv on first run) +``` + +## Run + +```bash +# one agent over all tasks (built-in templates: claude, codex) +python run_agents.py --agent claude --threads 4 + +# or a custom agent command (tokens: {agents_md} {agents_md_path} {task_dir} {task_id}) +python run_agents.py --cmd 'mytool run --prompt-file {agents_md_path}' --timeout 1200 + +# then aggregate +python collect.py # -> comparison.json / comparison.csv +``` + +**Ablation (no-harness root):** the agent runs with `verify` + `submit` only (no +`run_specharness.sh`). After all agents finish, score every dir's agent-written +`Solution.java` with the spec-harness it never had access to: + +```bash +VERIACT_PYTHON=/path/to/python OPENJML=/path/to/openjml \ + python score_all.py --threads 8 # -> harness_scores.json / harness_scores.csv +``` + +This also fills in each `submission.json`'s scores, so `python collect.py` +afterwards reflects them. (`collect.py --score-missing` does the same on the fly for +submissions that still lack scores.) + +Compare agents by running each into its **own** out-root (scaffold once per agent, +or copy this root), then diff the `comparison.csv` files. + +## Dependencies + +Each dir needs only the `javalang` pip package and the `openjml` binary on PATH. +The `*.sh` scripts self-bootstrap a `harness/.venv` on first run if `javalang` +isn't importable. Set `VERIACT_PYTHON=/path/to/python` to reuse an existing +interpreter and skip bootstrapping; set `OPENJML=/path/to/openjml` (or pass +`--openjml`) if it isn't on PATH. + +## Success criterion + +A task passes when `post_correctness >= 0.5` AND `post_completeness >= 0.5` +(recorded as `passed` in each `submission.json`). + +## Attempt budget + +Each task allows a fixed number of tool attempts (`verify` + `run_specharness` +calls), set at scaffold time and stored in `harness/config.json`. When exhausted, +the tools refuse and instruct the agent to submit. Override per run with +`AGENT_MAX_ATTEMPTS=N` (0 = unlimited). `submission.json` records `attempts` used. diff --git a/agent_harness/templates/run_agents.py b/agent_harness/templates/run_agents.py new file mode 100644 index 0000000..9116d86 --- /dev/null +++ b/agent_harness/templates/run_agents.py @@ -0,0 +1,172 @@ +#!/usr/bin/env python3 +"""Parent-level driver — fan out one fresh agent session per task directory. + +Run this from the out-root produced by ``agent_harness.scaffold``. For each task +subdir (any immediate child containing ``AGENTS.md``) it launches a headless +coding-agent session with that subdir as the working directory, feeding the dir's +``AGENTS.md`` as the prompt. One isolated session per task, matching VeriAct's +per-task runs — so VeriAct / Claude Code / Codex are all driven identically. + +This script is self-contained (stdlib only); it ships inside the out-root. + +Default models +-------------- + --agent claude -> Claude Code on claude-sonnet-4-6 + --agent codex -> Codex on the model from ~/.codex/config.toml (no -m passed) + +Examples +-------- + # Claude Code (Sonnet 4.6 by default), headless, auto-approve: + python run_agents.py --agent claude --threads 4 --only-missing + # expands to: claude -p {agents_md} --dangerously-skip-permissions --model claude-sonnet-4-6 + + # Codex (model from ~/.codex/config.toml, no bwrap sandbox): + python run_agents.py --agent codex --threads 4 --only-missing + # expands to: codex exec --skip-git-repo-check --dangerously-bypass-approvals-and-sandbox {agents_md} + + # Pin a model / override any flag with --cmd: + python run_agents.py --cmd 'claude -p {agents_md} --dangerously-skip-permissions --model claude-opus-4-8' + python run_agents.py --cmd 'codex exec --skip-git-repo-check --dangerously-bypass-approvals-and-sandbox --model gpt-5-codex {agents_md}' + python run_agents.py --cmd 'mytool run --prompt-file {agents_md_path}' --timeout 1200 +""" + +from __future__ import annotations + +import argparse +import os +import shlex +import subprocess +import sys +from concurrent.futures import ThreadPoolExecutor, as_completed + +ROOT = os.path.dirname(os.path.abspath(__file__)) + +# Built-in agent command templates. Tokens are replaced per task: +# {agents_md} -> full text of the dir's AGENTS.md (single argv token) +# {agents_md_path} -> absolute path to AGENTS.md +# {task_dir} -> absolute path to the task directory +# {task_id} -> directory name +# +# These run headless and must edit files + run the *.sh tools WITHOUT prompting, +# so they include each CLI's "auto-approve" flag and a default model. Only run on an +# isolated/sandboxed host. Override flags or the model with --cmd if your CLI version +# differs. +BUILTIN_AGENTS = { + "claude": "claude -p {agents_md} --dangerously-skip-permissions --model claude-sonnet-4-6", + # Codex runs WITHOUT its bubblewrap sandbox: in many containers/VMs bwrap cannot + # create its loopback ("RTM_NEWADDR: Operation not permitted"), which makes every + # file edit / command fail. --dangerously-bypass-approvals-and-sandbox avoids bwrap + # entirely (safe only on an already-isolated host, like the claude default). + # No -m: the model comes from your Codex config (~/.codex/config.toml). Override + # per run with --cmd '... -m ...' if needed. Note gpt-4o requires an OpenAI + # API-key login (a ChatGPT-account login rejects it). + "codex": ( + "codex exec --skip-git-repo-check " + "--dangerously-bypass-approvals-and-sandbox {agents_md}" + ), +} + + +def find_task_dirs() -> list[str]: + dirs = [] + for name in sorted(os.listdir(ROOT)): + d = os.path.join(ROOT, name) + if os.path.isdir(d) and os.path.exists(os.path.join(d, "AGENTS.md")): + dirs.append(d) + return dirs + + +def build_command(template: str, task_dir: str) -> list[str]: + agents_md_path = os.path.join(task_dir, "AGENTS.md") + with open(agents_md_path) as fh: + agents_md = fh.read() + tokens = shlex.split(template) + repl = { + "{agents_md}": agents_md, + "{agents_md_path}": agents_md_path, + "{task_dir}": task_dir, + "{task_id}": os.path.basename(task_dir), + } + out = [] + for tok in tokens: + for k, v in repl.items(): + tok = tok.replace(k, v) + out.append(tok) + return out + + +def run_one(template: str, task_dir: str, timeout: int | None) -> tuple[str, int, str]: + task_id = os.path.basename(task_dir) + cmd = build_command(template, task_dir) + log_path = os.path.join(task_dir, "harness", "agent_run.log") + os.makedirs(os.path.dirname(log_path), exist_ok=True) + try: + with open(log_path, "w") as log: + proc = subprocess.run( + cmd, + cwd=task_dir, + stdout=log, + stderr=subprocess.STDOUT, + timeout=timeout, + ) + return task_id, proc.returncode, log_path + except subprocess.TimeoutExpired: + return task_id, -1, log_path + " (timeout)" + except FileNotFoundError as exc: + return task_id, -2, f"command not found: {exc}" + + +def build_parser() -> argparse.ArgumentParser: + p = argparse.ArgumentParser(description="Drive an agent over scaffolded task dirs.") + g = p.add_mutually_exclusive_group(required=True) + g.add_argument("--agent", choices=sorted(BUILTIN_AGENTS), help="built-in agent template") + g.add_argument("--cmd", help="custom command template (see token list in --help)") + p.add_argument("--task-ids", help="file with task ids to run (one per line)") + p.add_argument("--threads", type=int, default=1, help="parallel sessions (default: 1)") + p.add_argument("--timeout", type=int, default=None, help="per-task timeout seconds") + p.add_argument( + "--only-missing", + action="store_true", + help="skip dirs that already have submission.json", + ) + return p + + +def main(argv: list[str] | None = None) -> int: + args = build_parser().parse_args(argv) + template = args.cmd or BUILTIN_AGENTS[args.agent] + + task_dirs = find_task_dirs() + if args.task_ids: + with open(args.task_ids) as fh: + wanted = {ln.strip() for ln in fh if ln.strip()} + task_dirs = [d for d in task_dirs if os.path.basename(d) in wanted] + if args.only_missing: + task_dirs = [ + d for d in task_dirs if not os.path.exists(os.path.join(d, "submission.json")) + ] + + if not task_dirs: + print("No task dirs to run.", file=sys.stderr) + return 1 + + print(f"Running '{template}' over {len(task_dirs)} task(s), threads={args.threads}") + results: list[tuple[str, int, str]] = [] + with ThreadPoolExecutor(max_workers=args.threads) as pool: + futs = { + pool.submit(run_one, template, d, args.timeout): d for d in task_dirs + } + for fut in as_completed(futs): + task_id, rc, log = fut.result() + status = "ok" if rc == 0 else f"rc={rc}" + print(f" [{status:>6}] {task_id} ({log})") + results.append((task_id, rc, log)) + + ok = sum(1 for _, rc, _ in results if rc == 0) + print(f"Done: {ok}/{len(results)} sessions exited 0. " + f"Next: python collect.py") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/agent_harness/templates/run_specharness.sh b/agent_harness/templates/run_specharness.sh new file mode 100644 index 0000000..25f4233 --- /dev/null +++ b/agent_harness/templates/run_specharness.sh @@ -0,0 +1,6 @@ +#!/usr/bin/env bash +# run_spec_harness — score the spec on the four spec-harness metrics. +set -euo pipefail +SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" +source "$SCRIPT_DIR/harness/_env.sh" +exec "$PYTHON" "$SCRIPT_DIR/harness/cli.py" harness "$@" diff --git a/agent_harness/templates/score_all.py b/agent_harness/templates/score_all.py new file mode 100644 index 0000000..c25717b --- /dev/null +++ b/agent_harness/templates/score_all.py @@ -0,0 +1,150 @@ +#!/usr/bin/env python3 +"""Post-hoc spec-harness scoring for every task dir in this out-root. + +Intended for the **no-harness** ablation arm: after the agents finish, run this +once to score each dir's agent-written ``Solution.java`` with the spec-harness (the +tool the agent never had access to) and store the four metrics. Works for the +with-harness arm too — it simply re-scores the final code. + +For each task dir it invokes the vendored ``harness/cli.py harness --no-budget`` +(so scoring never counts against the agent's attempt budget), then writes: + + * ``harness_scores.json`` / ``harness_scores.csv`` — the results table + * updates each dir's ``submission.json`` (scores + passed) when present, so + ``collect.py`` reflects the post-hoc scores too. + +Honors ``$VERIACT_PYTHON`` / ``$OPENJML`` (or ``--python`` / ``--openjml``). +Self-contained (stdlib only); ships inside the out-root. + +Examples +-------- + VERIACT_PYTHON=/path/.venv/bin/python OPENJML=/path/openjml python score_all.py + python score_all.py --threads 8 --openjml /path/openjml +""" + +from __future__ import annotations + +import argparse +import csv +import json +import os +import subprocess +import sys +from concurrent.futures import ThreadPoolExecutor, as_completed + +ROOT = os.path.dirname(os.path.abspath(__file__)) +METRICS = ["post_correctness", "post_completeness", "pre_correctness", "pre_completeness"] +THRESHOLD = 0.50 + + +def find_task_dirs() -> list[str]: + dirs = [] + for name in sorted(os.listdir(ROOT)): + d = os.path.join(ROOT, name) + if os.path.isdir(d) and os.path.exists(os.path.join(d, "harness", "cli.py")): + dirs.append(d) + return dirs + + +def score_dir(task_dir: str, python: str, openjml: str | None, timeout: int) -> dict: + task_id = os.path.basename(task_dir) + cli = os.path.join(task_dir, "harness", "cli.py") + cmd = [python, cli, "harness", "--no-budget"] + if openjml: + cmd += ["--openjml", openjml] + row: dict = {"task_id": task_id, **{m: None for m in METRICS}, "passed": False, + "error": None} + try: + proc = subprocess.run( + cmd, cwd=task_dir, capture_output=True, text=True, timeout=timeout + ) + data = json.loads(proc.stdout) + metrics = data.get(task_id) or next( + (v for k, v in data.items() if k != "_budget"), None + ) + if not isinstance(metrics, dict): + row["error"] = data.get("error", "no scores") + return row + for m in METRICS: + row[m] = metrics.get(m) + row["passed"] = ( + (metrics.get("post_correctness") or 0.0) >= THRESHOLD + and (metrics.get("post_completeness") or 0.0) >= THRESHOLD + ) + _update_submission(task_dir, task_id, metrics, row["passed"]) + except subprocess.TimeoutExpired: + row["error"] = "timeout" + except (subprocess.SubprocessError, json.JSONDecodeError, ValueError) as exc: + row["error"] = str(exc) + return row + + +def _update_submission(task_dir: str, task_id: str, metrics: dict, passed: bool) -> None: + sub = os.path.join(task_dir, "submission.json") + if not os.path.exists(sub): + return + try: + with open(sub) as fh: + data = json.load(fh) + data["scores"] = {m: metrics.get(m) for m in METRICS} + data["passed"] = passed + with open(sub, "w") as fh: + json.dump(data, fh, indent=2) + except (OSError, json.JSONDecodeError): + pass + + +def main(argv: list[str] | None = None) -> int: + p = argparse.ArgumentParser(description="Score every task dir's Solution.java.") + p.add_argument("--threads", type=int, default=4, help="parallel scorers (default: 4)") + p.add_argument("--timeout", type=int, default=1800, help="per-task timeout seconds") + p.add_argument("--python", help="interpreter to run harness/cli.py (default: $VERIACT_PYTHON or 'python')") + p.add_argument("--openjml", help="OpenJML binary (default: $OPENJML)") + p.add_argument("--out", default=os.path.join(ROOT, "harness_scores"), + help="output path prefix (default: ./harness_scores)") + args = p.parse_args(argv) + + python = args.python or os.environ.get("VERIACT_PYTHON", "python") + openjml = args.openjml or os.environ.get("OPENJML") + + task_dirs = find_task_dirs() + if not task_dirs: + print("No task dirs found.", file=sys.stderr) + return 1 + + print(f"Scoring {len(task_dirs)} task(s) with spec-harness, threads={args.threads}") + rows: list[dict] = [] + with ThreadPoolExecutor(max_workers=args.threads) as pool: + futs = { + pool.submit(score_dir, d, python, openjml, args.timeout): d + for d in task_dirs + } + for fut in as_completed(futs): + row = fut.result() + rows.append(row) + tag = "err:" + row["error"] if row["error"] else f"pass={row['passed']}" + print(f" [{tag}] {row['task_id']}") + + rows.sort(key=lambda r: r["task_id"]) + fields = ["task_id", *METRICS, "passed", "error"] + with open(args.out + ".json", "w") as fh: + json.dump(rows, fh, indent=2) + with open(args.out + ".csv", "w", newline="") as fh: + w = csv.DictWriter(fh, fieldnames=fields) + w.writeheader() + w.writerows(rows) + + scored = [r for r in rows if r["error"] is None] + passed = sum(1 for r in scored if r["passed"]) + avg = { + m: round(sum(r[m] for r in scored if r[m] is not None) / len(scored), 3) + if scored else 0.0 + for m in METRICS + } + print(f"Scored {len(scored)}/{len(rows)} (passed={passed}); avg: {avg}") + print(f" -> {args.out}.json / {args.out}.csv") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/agent_harness/templates/submit.sh b/agent_harness/templates/submit.sh new file mode 100644 index 0000000..3ea62bd --- /dev/null +++ b/agent_harness/templates/submit.sh @@ -0,0 +1,6 @@ +#!/usr/bin/env bash +# submit — record the final submission (writes submission.json). +set -euo pipefail +SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" +source "$SCRIPT_DIR/harness/_env.sh" +exec "$PYTHON" "$SCRIPT_DIR/harness/cli.py" submit "$@" diff --git a/agent_harness/templates/verifier_tool.py b/agent_harness/templates/verifier_tool.py new file mode 100644 index 0000000..6095931 --- /dev/null +++ b/agent_harness/templates/verifier_tool.py @@ -0,0 +1,283 @@ +import logging +import os +import re +import signal +import subprocess +import tempfile +import uuid +from dataclasses import dataclass, field +from typing import Any, Optional + +logger = logging.getLogger("veriact_verifier_tool") + + + +# TASK SCHEMA +@dataclass +class TestCase: + input: str + output: str + + @classmethod + def from_dict(cls, data: dict[str, str]) -> "TestCase": + return cls(input=data["input"], output=data["output"]) + + +@dataclass +class Task: + task_id: str + code: str + class_name: str + test_name: str + javadoc: str + category: str + origin_id: str + test_code: str = "" + test_inputs: list[TestCase] = field(default_factory=list) + generated_test_cases: list[TestCase] = field(default_factory=list) + + @classmethod + def from_dict(cls, data: dict[str, Any]) -> "Task": + return cls( + task_id=data["task_id"], + code=data["code"], + class_name=data["class_name"], + test_name=data["test_name"], + javadoc=data["javadoc"], + category=data["category"], + origin_id=data["origin_id"], + test_code=data.get("test_code", ""), + test_inputs=[TestCase.from_dict(tc) for tc in data.get("test_inputs", [])], + generated_test_cases=[ + TestCase.from_dict(tc) for tc in data.get("generated_test_cases", []) + ], + ) + + + +# ERROR CLASSIFICATION +def extract_errors(error_message: str) -> list[tuple[str, str]]: + pattern = r"(/tmp/[^:]+:\d+: )(\w+):" + matches = re.split(r"(?=/tmp/[^:]+:\d+: \w+:)", error_message) + errors = [] + for match in matches: + if match.strip(): + level_match = re.search(pattern, match) + if level_match: + error_level = level_match.group(2) + if error_level != "warning": + if ( + "Associated declaration:" in match + or "Associated method exit" in match + ): + if len(errors) == 0: + continue + errors[-1] = (errors[-1][0], errors[-1][1] + match) + else: + errors.append((error_level, match.strip())) + return errors + + +def verification_failure_map(error_message: str) -> str: + mapping = [ + ("LoopInvariantBeforeLoop", "LoopInvariantFailure"), + ("ArithmeticOperationRange", "ArithmeticOperationRange"), + ("Assignable", "AssignableFailure"), + ("Postcondition:", "PostconditionFailure"), + ("Assert)", "AssertFailure"), + ("UndefinedNullDeReference", "NullDeReference"), + ("PossiblyNullDeReference", "NullDeReference"), + ("LoopInvariant)", "LoopInvariantFailure"), + ("PossiblyNegativeIndex", "ArrayIndex"), + ("PossiblyNegativeSize", "NegativeSize"), + ("PossiblyTooLargeIndex", "ArrayIndex"), + ("LoopDecreases", "RankingFunctionFailure"), + ("PossiblyBadArrayAssignment", "BadArrayAssignment"), + ("Precondition:", "PreconditionFailure"), + ("Precondition conjunct is false:", "PreconditionFailure"), + ("UndefinedTooLargeIndex", "ArrayIndex"), + ("PossiblyDivideByZero", "DivideByZero"), + ("PossiblyBadCast", "BadCast"), + ("UndefinedDivideByZero", "DivideByZero"), + ("ExceptionalPostcondition:", "ExceptionalPostconditionFailure"), + ("UndefinedCalledMethodPrecondition:", "CalledMethodPrecondition"), + ("UndefinedNegativeIndex", "ArrayIndex"), + ("PossiblyNullUnbox", "NullUnbox"), + ("LoopDecreasesNonNegative", "RankingFunctionFailure"), + ("Postcondition)", "PostconditionFailure"), + ("ArithmeticCastRange", "ArithmeticCastRange"), + ("UndefinedNullUnbox", "NullUnbox"), + ("PossiblyLargeShift", "LargeShift"), + ] + for pat, failure_type in mapping: + if pat in error_message: + return failure_type + return "UnknownVerificationFailure" + + +def classify_failures(error_level: str, error_message: str) -> str: + if error_level == "error": + return "SyntaxError" + elif error_level == "verify": + return verification_failure_map(error_message) + else: + return "UnknownError" + + + +# OPENJML VERIFICATION +@dataclass +class VerificationResult: + success: bool + error_log: str + return_code: int + classified_errors: list[dict] = field(default_factory=list) + + +def write_to_file(content: str, filepath: str) -> None: + os.makedirs(os.path.dirname(filepath), exist_ok=True) + with open(filepath, "w") as f: + f.write(content) + + +def verify_with_openjml( + code_with_spec: str, + classname: str, + timeout: int = 180, + output_dir: str = "veriact_outputs/tmp", +) -> VerificationResult: + + run_id = uuid.uuid4().hex + output_dir = os.path.join(output_dir, f"veriact_{run_id}") + os.makedirs(output_dir, exist_ok=True) + + tmp_filename = os.path.join(output_dir, f"{classname}.java") + write_to_file(code_with_spec, tmp_filename) + + cmd = [ + "openjml", + "--esc", + "--esc-max-warnings", + "1", + "--prover=cvc4", + "--nonnull-by-default", + "--arithmetic-failure=quiet", + "-nowarn", + tmp_filename, + ] + + proc = subprocess.Popen( + cmd, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + text=True, + preexec_fn=os.setsid, + ) + + try: + stdout, stderr = proc.communicate(timeout=timeout) + raw_output = stdout + stderr + return_code = proc.returncode + return return_verification_result(raw_output, return_code) + except subprocess.TimeoutExpired: + raw_output = ( + f"Timeout: OpenJML verification exceeded time limit of {timeout} seconds" + ) + return_code = 1 + return return_verification_result(raw_output, return_code) + except Exception as e: + raw_output = f"Error: {str(e)}" + return_code = 1 + return return_verification_result(raw_output, return_code) + finally: + try: + os.killpg(os.getpgid(proc.pid), signal.SIGKILL) + except ProcessLookupError: + pass + + +def return_verification_result(raw_output: str, return_code: int) -> VerificationResult: + classified_errors = [] + if return_code != 0 and raw_output.strip(): + try: + errors = extract_errors(raw_output) + for error_level, error_msg in errors: + error_type = classify_failures(error_level, error_msg) + classified_errors.append({"type": error_type, "raw": error_msg[:500]}) + except Exception: + classified_errors.append({"type": "ParseError", "raw": raw_output[:500]}) + + success = return_code == 0 and len(classified_errors) == 0 + return VerificationResult( + success=success, + error_log=raw_output, + return_code=return_code, + classified_errors=classified_errors, + ) + + + +# GRADUATED SCORING +def compute_graduated_score(result: VerificationResult) -> float: + """ + Graduated scoring for optimization. Gives the optimizer a gradient. + + 1.0 - Verification passes + 0.3 - 1 verification error (almost correct) + 0.1 - 2+ verification errors (valid JML, semantically wrong) + 0.0 - Syntax error or empty output + """ + if result.success: + return 1.0 + if not result.classified_errors: + return 0.0 + + syntax_errors = [e for e in result.classified_errors if e["type"] == "SyntaxError"] + verification_errors = [ + e for e in result.classified_errors if e["type"] != "SyntaxError" + ] + + if syntax_errors: + return 0.0 + if len(verification_errors) == 1: + return 0.3 + return 0.1 + + + +# HELPERS +def clean_code_fences(text: str) -> str: + text = re.sub(r"```java\s*\n?", "", text) + text = re.sub(r"```\s*$", "", text) + return text.strip() + + +def format_error_feedback(result: VerificationResult, task_id: str) -> str: + if result.success: + return f"[PASS] Task '{task_id}': Specification verified by OpenJML." + + error_counts: dict[str, int] = {} + for err in result.classified_errors: + t = err["type"] + error_counts[t] = error_counts.get(t, 0) + 1 + + error_summary = ", ".join( + f"{t} (x{c})" if c > 1 else t for t, c in error_counts.items() + ) + + raw_log = result.error_log + if len(raw_log) > 800: + raw_log = raw_log[:800] + "\n... [truncated]" + + return ( + f"[FAIL] Task '{task_id}': {error_summary}\n" + f"--- OpenJML Log ---\n{raw_log}\n" + f"--- Fix Guidance ---\n" + f"SyntaxError: Fix JML syntax (missing semicolons, wrong keywords).\n" + f"PostconditionFailure: The @ensures clause is logically incorrect.\n" + f"LoopInvariantFailure: The @maintaining clause doesn't hold.\n" + f"RankingFunctionFailure: The @decreases expression is wrong.\n" + f"ArrayIndex: Missing array bounds check in @requires.\n" + f"NullDeReference: Missing null check in @requires.\n" + f"ArithmeticOperationRange: Integer overflow not guarded." + ) diff --git a/agent_harness/templates/verify.sh b/agent_harness/templates/verify.sh new file mode 100644 index 0000000..4a913ae --- /dev/null +++ b/agent_harness/templates/verify.sh @@ -0,0 +1,6 @@ +#!/usr/bin/env bash +# verify_with_openjml — run OpenJML ESC on Solution.java. +set -euo pipefail +SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" +source "$SCRIPT_DIR/harness/_env.sh" +exec "$PYTHON" "$SCRIPT_DIR/harness/cli.py" verify "$@" From eca2820e6f854b222e276f61bd1e1b9c13f303b9 Mon Sep 17 00:00:00 2001 From: MRHMisu Date: Sun, 28 Jun 2026 02:03:49 -0700 Subject: [PATCH 2/3] run harness on LLM response in a loop --- scripts/run_spec_harness_loop.sh | 36 ++++++++++++++++++++++++ veriact/{ => agent}/agent.py | 0 veriact/{ => core}/agent_types.py | 0 veriact/{ => core}/data_types.py | 0 veriact/{ => core}/file_utility.py | 0 veriact/{ => core}/memory.py | 0 veriact/{ => core}/models.py | 0 veriact/{ => core}/monitoring.py | 0 veriact/{ => core}/utility.py | 0 veriact/{ => run}/run_batch.py | 0 veriact/{ => run}/run_single.py | 0 veriact/{tools_base.py => tools/base.py} | 0 veriact/{ => tools}/default_tools.py | 0 veriact/{ => tools}/harness_tool.py | 0 veriact/{ => tools}/verifier_tool.py | 0 15 files changed, 36 insertions(+) create mode 100755 scripts/run_spec_harness_loop.sh rename veriact/{ => agent}/agent.py (100%) rename veriact/{ => core}/agent_types.py (100%) rename veriact/{ => core}/data_types.py (100%) rename veriact/{ => core}/file_utility.py (100%) rename veriact/{ => core}/memory.py (100%) rename veriact/{ => core}/models.py (100%) rename veriact/{ => core}/monitoring.py (100%) rename veriact/{ => core}/utility.py (100%) rename veriact/{ => run}/run_batch.py (100%) rename veriact/{ => run}/run_single.py (100%) rename veriact/{tools_base.py => tools/base.py} (100%) rename veriact/{ => tools}/default_tools.py (100%) rename veriact/{ => tools}/harness_tool.py (100%) rename veriact/{ => tools}/verifier_tool.py (100%) diff --git a/scripts/run_spec_harness_loop.sh b/scripts/run_spec_harness_loop.sh new file mode 100755 index 0000000..8cc8395 --- /dev/null +++ b/scripts/run_spec_harness_loop.sh @@ -0,0 +1,36 @@ +#!/usr/bin/env bash +set -euo pipefail + + +response_list_file="${1:?Usage: $0 spec_har_sgb_run_jsonl_test.txt}" + +basepath="/home/mdrh/experiments/all_approaches_result_jsonl" +benchmark_path="/home/mdrh/code/VeriAct/benchmarks/specgenbench/sgb.json" +openjml="openjml" +output_root="/home/mdrh/experiments/spec_harness_sgb_results_updated" +threads=12 +max_pairs=5 + +mkdir -p "$output_root" + +while IFS= read -r llm_response_path || [[ -n "$llm_response_path" ]]; do + [[ -z "$llm_response_path" ]] && continue + [[ "$llm_response_path" =~ ^# ]] && continue + + output_name="$(basename "$llm_response_path")" + output_name="${output_name%.jsonl}" + + python -m spec_harness.eval_llm_response \ + --benchmark_path "$benchmark_path" \ + --llm_response_path "$basepath/$llm_response_path" \ + --openjml "$openjml" \ + --output "$output_root/$output_name" \ + --threads "$threads" \ + --max-pairs "$max_pairs" \ + --verbose + + sleep 5 + pkill -f cvc4-1.6 || true + sleep 5 + +done < "$response_list_file" \ No newline at end of file diff --git a/veriact/agent.py b/veriact/agent/agent.py similarity index 100% rename from veriact/agent.py rename to veriact/agent/agent.py diff --git a/veriact/agent_types.py b/veriact/core/agent_types.py similarity index 100% rename from veriact/agent_types.py rename to veriact/core/agent_types.py diff --git a/veriact/data_types.py b/veriact/core/data_types.py similarity index 100% rename from veriact/data_types.py rename to veriact/core/data_types.py diff --git a/veriact/file_utility.py b/veriact/core/file_utility.py similarity index 100% rename from veriact/file_utility.py rename to veriact/core/file_utility.py diff --git a/veriact/memory.py b/veriact/core/memory.py similarity index 100% rename from veriact/memory.py rename to veriact/core/memory.py diff --git a/veriact/models.py b/veriact/core/models.py similarity index 100% rename from veriact/models.py rename to veriact/core/models.py diff --git a/veriact/monitoring.py b/veriact/core/monitoring.py similarity index 100% rename from veriact/monitoring.py rename to veriact/core/monitoring.py diff --git a/veriact/utility.py b/veriact/core/utility.py similarity index 100% rename from veriact/utility.py rename to veriact/core/utility.py diff --git a/veriact/run_batch.py b/veriact/run/run_batch.py similarity index 100% rename from veriact/run_batch.py rename to veriact/run/run_batch.py diff --git a/veriact/run_single.py b/veriact/run/run_single.py similarity index 100% rename from veriact/run_single.py rename to veriact/run/run_single.py diff --git a/veriact/tools_base.py b/veriact/tools/base.py similarity index 100% rename from veriact/tools_base.py rename to veriact/tools/base.py diff --git a/veriact/default_tools.py b/veriact/tools/default_tools.py similarity index 100% rename from veriact/default_tools.py rename to veriact/tools/default_tools.py diff --git a/veriact/harness_tool.py b/veriact/tools/harness_tool.py similarity index 100% rename from veriact/harness_tool.py rename to veriact/tools/harness_tool.py diff --git a/veriact/verifier_tool.py b/veriact/tools/verifier_tool.py similarity index 100% rename from veriact/verifier_tool.py rename to veriact/tools/verifier_tool.py From f4ca8cee8ed2f8b1758f543911ce366ddabe681e Mon Sep 17 00:00:00 2001 From: MRHMisu Date: Sun, 28 Jun 2026 02:05:59 -0700 Subject: [PATCH 3/3] transform veriact into a CLI agent --- pyproject.toml | 2 +- veriact/README.md | 165 ++-- veriact/__init__.py | 18 +- veriact/_function_type_hints_utils.py | 145 ---- veriact/agent/__init__.py | 6 + veriact/agent/agent.py | 174 ++-- veriact/agent/cli_agent.py | 582 +++++++++++++ veriact/codeact.py | 821 ------------------ veriact/config.py | 21 +- veriact/core/__init__.py | 0 veriact/core/memory.py | 6 +- veriact/core/models.py | 4 +- veriact/core/monitoring.py | 2 +- .../veriact_cli_no_harness_prompt.yaml | 138 +++ veriact/prompts/veriact_cli_prompt.yaml | 156 ++++ veriact/prompts/veriact_prompt.yaml | 166 ---- veriact/run/__init__.py | 0 veriact/run/run_batch.py | 8 +- veriact/run/run_single.py | 6 +- veriact/run/score_no_harness.py | 140 +++ veriact/tool_validation.py | 112 --- veriact/tools.py | 232 ----- veriact/tools/__init__.py | 0 veriact/tools/base.py | 50 +- veriact/tools/cli.py | 196 +++++ veriact/tools/default_tools.py | 2 +- veriact/tools/descriptors.py | 52 ++ 27 files changed, 1517 insertions(+), 1687 deletions(-) delete mode 100644 veriact/_function_type_hints_utils.py create mode 100644 veriact/agent/__init__.py create mode 100644 veriact/agent/cli_agent.py delete mode 100644 veriact/codeact.py create mode 100644 veriact/core/__init__.py create mode 100644 veriact/prompts/veriact_cli_no_harness_prompt.yaml create mode 100644 veriact/prompts/veriact_cli_prompt.yaml delete mode 100644 veriact/prompts/veriact_prompt.yaml create mode 100644 veriact/run/__init__.py create mode 100644 veriact/run/score_no_harness.py delete mode 100644 veriact/tool_validation.py delete mode 100644 veriact/tools.py create mode 100644 veriact/tools/__init__.py create mode 100644 veriact/tools/cli.py create mode 100644 veriact/tools/descriptors.py diff --git a/pyproject.toml b/pyproject.toml index c34be0d..bd3b718 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -77,4 +77,4 @@ lines-after-imports = 2 "veriact.prompts" = ["*.yaml"] [project.scripts] -veriact = "veriact.cli:main" +veriact = "veriact.tools.cli:main" diff --git a/veriact/README.md b/veriact/README.md index f319702..bd43e47 100644 --- a/veriact/README.md +++ b/veriact/README.md @@ -1,111 +1,100 @@ -# VeriAct -Verification-guided correct & complete formal specification synthesis. The agent iteratively writes JML specifications, verifies them with OpenJML, and evaluates correctness/completeness with Spec-Harness until the specifications pass both checks. +# veriact -## How It Works +A CLI-driven refactor of VeriAct. Same verification-guided JML spec-synthesis loop +and the same memory / monitoring / trajectory recording, but the agent now drives +**command-line tools** in a think → run-CLI → observe ReAct loop instead of +executing Python via CodeAct. -``` -run_single.py / run_batch.py - │ - ▼ - VeriActAgent ← loads tools, wraps CodeAgent - │ - ▼ - CodeAgent ← ReAct loop: think → execute Python code → observe - │ - ┌────┴──────────────────────────┐ - ▼ ▼ -verify_with_openjml run_spec_harness - (verifier_tool.py) (harness_tool.py) - │ │ - OpenJML (ESC) Spec-Harness evaluation - post/pre correctness & completeness -``` - -Each step the agent outputs `{"thought": "...", "code": "..."}`. The code runs in a sandboxed Python environment and calls tools directly. The agent succeeds when `post_correctness ≥ 0.5` AND `post_completeness ≥ 0.5` and calls `task_complete`. +## What changed vs `veriact/` -## Module Reference +| | `veriact/` (CodeAct) | `veriact/` (CLI-ReAct) | +|---|---|---| +| Agent action | emits `{thought, code}`; Python runs in a sandbox and calls tool objects | emits `{thought, tool, tool_input}`; the tool CLI runs as a **subprocess**, stdout is the observation | +| Tools | 4 (`verify_with_openjml`, `analyze_openjml_errors`, `run_spec_harness`, `task_complete`) | **3** (`verify` with analyze merged in, `run_spec_harness`, `task_complete`) | +| Code execution | in-process `exec` with AST safety checks | none — only CLI subprocesses | +| Memory / monitoring / trajectory | preserved | **preserved, unchanged** | -| File | What it does | -|------|-------------| -| `agent.py` | `VeriActAgent` — top-level entry point; wraps `CodeAgent`, checks harness threshold, writes output | -| `codeact.py` | `CodeAgent` / `MultiStepAgent` — ReAct loop; executes agent-generated Python code in a sandboxed namespace | -| `data_types.py` | `Task`, `TestCase`, `HARNESS_PASS_THRESHOLD = 0.5` | -| `models.py` | LLM backends: `OpenAIServerModel`, `AnthropicModel`, `GeminiModel`, `VLLMModel` | -| `tools.py` | `get_veriact_tools()` — returns the three agent tools (see below) | -| `tools_base.py` | `Tool` base class with input validation and type checking | -| `verifier_tool.py` | `verify_with_openjml()` — writes code to disk, runs OpenJML ESC, parses and classifies errors | -| `harness_tool.py` | `evaluate_problem()` — runs Spec-Harness, returns the four metric scores | -| `memory.py` | `ActionStep`, `AgentMemory` — records each agent step for logging and replay | -| `agent_types.py` | `AgentText` type wrapper for agent I/O | -| `prompts/veriact_prompt.yaml` | System prompt: role, tool descriptions, workflow, timeout strategy | +The three tools are the subcommands of [`cli.py`](veriact/cli.py): -## Agent Tools +- `verify` — OpenJML ESC; output includes the error analysis (`failure_modes`, + `repair_hints`, `summary`), so the separate analyze tool is gone. +- `harness` — the four spec-harness metrics. +- `submit` — records the final submission (`task_complete`). -| Tool name | Inputs | Returns | -|-----------|--------|---------| -| `verify_with_openjml` | `jml_annotated_code: str` | `{verified, return_code, errors, raw_output}` | -| `analyze_openjml_errors` | `openjml_log: str` | `{failure_modes, repair_hints, summary}` | -| `run_spec_harness` | `task_id: str`, `jml_annotated_code: str` | `{post_correctness, post_completeness, pre_correctness, pre_completeness}` | -| `task_complete` | — | signals successful completion | +The agent supplies the full annotated code in `tool_input.jml_annotated_code` each +step; the agent writes it to `Solution.java` in a per-task workspace and runs the +CLI against it. There is **no attempt budget** here — the loop is bounded by +`--max-steps` (each tool call ≈ one step, matching VeriAct). +## Run (same UX as VeriAct) -## Usage +Run from the repo root. ```bash -cd VeriAct +# one task at a time +python -m veriact.run.run_single \ + --benchmark benchmarks/specgenbench/sgb.json \ + --model gpt-4o --output-dir out --openjml-path openjml \ + --max-steps 15 --planning_interval 5 -# Sequential — one task at a time -python -m veriact.run_single.py \ +# parallel +python -m veriact.run.run_batch \ --benchmark benchmarks/specgenbench/sgb.json \ - --model gpt-4o \ - --output-dir \ - --max-steps 15 \ - --planning_interval 3 + --model gpt-4o --threads 4 --output-dir out --max-steps 15 +``` +### Ablation: no-harness -# Parallel -python -m veriact.run_batch.py \ - --benchmark benchmarks/specgenbench/sgb.json \ - --model gpt-4o \ - --threads 4 \ - --output-dir \ - --max-steps 15 +Pass `--no-harness` to either runner to run with **only `verify` + `task_complete`** +(no `run_spec_harness`). It uses `prompts/veriact_cli_no_harness_prompt.yaml` and +success is defined as **verification passing** (last `verify` returns `verified: +true`). If the model calls `run_spec_harness` anyway, the tool replies that it is +unavailable. + +```bash +python -m veriact.run.run_batch --benchmark benchmarks/specgenbench/sgb.json \ + --model gpt-4o --threads 4 --output-dir out_nh --max-steps 15 --no-harness ``` -| Flag | Default | Description | -|------|---------|-------------| -| `--benchmark` | required | Dataset JSON/JSONL path | -| `--model` | `gpt-4o` | LLM model ID — provider auto-detected from prefix (`gpt-`/`claude-`/`gemini-`) | -| `--output-dir` | `veriact_outputs` | Output directory | -| `--openjml-path` | `openjml` | Path to OpenJML binary | -| `--max-steps` | 15 | Max agent iterations per task | -| `--planning_interval` | 5 | Steps between planning phases | -| `--threads` | 4 | Parallel workers (`run_batch.py` only) | -| `--task-ids` | — | File with task IDs to filter (`run_batch.py` only) | +**Scoring the no-harness output offline.** Since the no-harness arm never runs the +spec-harness, score its final specs afterward for comparison against the harness +arm. `score_no_harness` walks `/workspaces//Solution.java` and +writes `harness_scores.{json,csv}`: -Set `VLLM_API_BASE` environment variable to use a local vLLM server. +```bash +python -m veriact.run.score_no_harness \ + --run-dir out_nh/veriact__gpt-4o__ \ + --openjml openjml --threads 4 +``` -## Output +Outputs match VeriAct's layout: `out//trajectories.jsonl`, +`out//trajectories/_veriact_trajectory.json`, and per-task +workspaces under `out//workspaces//` (Solution.java, Test.java, +harness/task.json, submission.json, stubs). -Each run produces: +## Layout ``` -/ -├── trajectories.jsonl # One JSON object per task -├── trajectories/ -│ └── _veriact_trajectory.json -└── failed_tasks.json # Tasks that errored (if any) +veriact/ + __init__.py config.py README.md + agent/ + agent.py # VeriActAgent: workspace setup + trajectory (entry point) + cli_agent.py # MultiStepAgent + CLIAgent (the ReAct-over-CLI loop) + tools/ + cli.py # the 3 tools as CLI subcommands (verify | harness | submit) + descriptors.py # tool descriptors (name/description/inputs) for prompts + base.py # Tool base class + default_tools.py # task_complete + harness_tool.py # spec-harness scorer + verifier_tool.py # OpenJML verifier + run/ + run_single.py run_batch.py + prompts/ + veriact_cli_prompt.yaml + core/ + memory.py monitoring.py models.py data_types.py + agent_types.py file_utility.py utility.py ``` -Each entry in `trajectories.jsonl`: - -```json -{ - "task_id": "...", - "success": true, - "iterations": 7, - "agent_output": "...", - "agent_dict": { ... }, - "_last_attempted_code": "..." -} -``` +The OpenJML flags, mutant budget (k=5), and `max_pairs=5` in `tools/harness_tool.py` +and `tools/verifier_tool.py` match the original VeriAct scorer/verifier. diff --git a/veriact/__init__.py b/veriact/__init__.py index 4b6c77a..ba1fcb1 100644 --- a/veriact/__init__.py +++ b/veriact/__init__.py @@ -1,17 +1,19 @@ """ -VeriAct — Verification-Guided Agentic Framework for Formal Specification Synthesis. +veriact — CLI-driven refactor of VeriAct. -Usage: - from veriact import VeriActAgent, OpenAIServerModel +Same verification-guided spec-synthesis loop, but the agent drives **command-line +tools** (verify, run_spec_harness, task_complete) in a think → run-CLI → observe +ReAct loop, instead of executing Python via CodeAct. Memory, monitoring, and +trajectory recording are preserved. - model = OpenAIServerModel(model_id="gpt-4o") - agent = VeriActAgent(model=model) - result = agent.run(task) + from veriact import VeriActAgent, OpenAIServerModel + agent = VeriActAgent(model=OpenAIServerModel(model_id="gpt-4o")) + agent.run(task) """ from veriact.agent import VeriActAgent -from veriact.data_types import Task, HARNESS_PASS_THRESHOLD -from veriact.models import ( +from veriact.core.data_types import Task, HARNESS_PASS_THRESHOLD +from veriact.core.models import ( OpenAIServerModel, AnthropicModel, GeminiModel, diff --git a/veriact/_function_type_hints_utils.py b/veriact/_function_type_hints_utils.py deleted file mode 100644 index c159a38..0000000 --- a/veriact/_function_type_hints_utils.py +++ /dev/null @@ -1,145 +0,0 @@ -"""Utilities for parsing type hints into JSON schemas. Derived from transformers.""" - -import inspect -import json -import re -import types -from copy import copy -from typing import Any, Callable, Dict, List, Optional, Tuple, Union, get_args, get_origin, get_type_hints - - -def get_imports(code: str) -> List[str]: - code = re.sub(r"\s*try\s*:.*?except.*?:", "", code, flags=re.DOTALL) - code = re.sub(r"if is_flash_attn[a-zA-Z0-9_]+available\(\):\s*(from flash_attn\s*.*\s*)+", "", code, flags=re.MULTILINE) - imports = re.findall(r"^\s*import\s+(\S+?)(?:\s+as\s+\S+)?\s*$", code, flags=re.MULTILINE) - imports += re.findall(r"^\s*from\s+(\S+)\s+import", code, flags=re.MULTILINE) - imports = [imp.split(".")[0] for imp in imports if not imp.startswith(".")] - return list(set(imports)) - - -class TypeHintParsingException(Exception): - pass - -class DocstringParsingException(Exception): - pass - - -def get_json_schema(func: Callable) -> Dict: - doc = inspect.getdoc(func) - if not doc: - raise DocstringParsingException(f"Cannot generate JSON schema for {func.__name__} because it has no docstring!") - doc = doc.strip() - main_doc, param_descriptions, return_doc = _parse_google_format_docstring(doc) - json_schema = _convert_type_hints_to_json_schema(func) - if (return_dict := json_schema["properties"].pop("return", None)) is not None: - if return_doc is not None: - return_dict["description"] = return_doc - for arg, schema in json_schema["properties"].items(): - if arg not in param_descriptions: - raise DocstringParsingException(f"Cannot generate JSON schema for {func.__name__} because the docstring has no description for the argument '{arg}'") - desc = param_descriptions[arg] - enum_choices = re.search(r"\(choices:\s*(.*?)\)\s*$", desc, flags=re.IGNORECASE) - if enum_choices: - schema["enum"] = [c.strip() for c in json.loads(enum_choices.group(1))] - desc = enum_choices.string[: enum_choices.start()].strip() - schema["description"] = desc - output = {"name": func.__name__, "description": main_doc, "parameters": json_schema} - if return_dict is not None: - output["return"] = return_dict - return {"type": "function", "function": output} - - -description_re = re.compile(r"^(.*?)[\n\s]*(Args:|Returns:|Raises:|\Z)", re.DOTALL) -args_re = re.compile(r"\n\s*Args:\n\s*(.*?)[\n\s]*(Returns:|Raises:|\Z)", re.DOTALL) -args_split_re = re.compile( - r"(?:^|\n)\s*(\w+)\s*(?:\([^)]*?\))?:\s*(.*?)\s*(?=\n\s*\w+\s*(?:\([^)]*?\))?:|\Z)", - re.DOTALL | re.VERBOSE, -) -returns_re = re.compile(r"\n\s*Returns:\n\s*(?:[^)]*?:\s*)?(.*?)[\n\s]*(Raises:|\Z)", re.DOTALL) - - -def _parse_google_format_docstring(docstring: str) -> Tuple[Optional[str], Optional[Dict], Optional[str]]: - description_match = description_re.search(docstring) - args_match = args_re.search(docstring) - returns_match = returns_re.search(docstring) - description = description_match.group(1).strip() if description_match else None - docstring_args = args_match.group(1).strip() if args_match else None - returns = returns_match.group(1).strip() if returns_match else None - if docstring_args is not None: - docstring_args = "\n".join([line for line in docstring_args.split("\n") if line.strip()]) - matches = args_split_re.findall(docstring_args) - args_dict = {match[0]: re.sub(r"\s*\n+\s*", " ", match[1].strip()) for match in matches} - else: - args_dict = {} - return description, args_dict, returns - - -def _convert_type_hints_to_json_schema(func: Callable, error_on_missing_type_hints: bool = True) -> Dict: - type_hints = get_type_hints(func) - signature = inspect.signature(func) - properties = {} - for param_name, param_type in type_hints.items(): - properties[param_name] = _parse_type_hint(param_type) - required = [] - for param_name, param in signature.parameters.items(): - if param.annotation == inspect.Parameter.empty and error_on_missing_type_hints: - raise TypeHintParsingException(f"Argument {param.name} is missing a type hint in function {func.__name__}") - if param_name not in properties: - properties[param_name] = {} - if param.default == inspect.Parameter.empty: - required.append(param_name) - else: - properties[param_name]["nullable"] = True - schema = {"type": "object", "properties": properties} - if required: - schema["required"] = required - return schema - - -def _parse_type_hint(hint: str) -> Dict: - origin = get_origin(hint) - args = get_args(hint) - if origin is None: - try: - return _get_json_schema_type(hint) - except KeyError: - raise TypeHintParsingException("Couldn't parse this type hint: ", hint) - elif origin is Union or (hasattr(types, "UnionType") and origin is types.UnionType): - subtypes = [_parse_type_hint(t) for t in args if t is not type(None)] - if len(subtypes) == 1: - return_dict = subtypes[0] - elif all(isinstance(subtype["type"], str) for subtype in subtypes): - return_dict = {"type": sorted([subtype["type"] for subtype in subtypes])} - else: - return_dict = {"anyOf": subtypes} - if type(None) in args: - return_dict["nullable"] = True - return return_dict - elif origin is list: - if not args: - return {"type": "array"} - return {"type": "array", "items": _parse_type_hint(args[0])} - elif origin is tuple: - if not args: - return {"type": "array"} - if len(args) == 1: - raise TypeHintParsingException(f"Single-element Tuple not supported: {hint}") - if ... in args: - raise TypeHintParsingException("Ellipsis in Tuple not supported. Use List[] instead.") - return {"type": "array", "prefixItems": [_parse_type_hint(t) for t in args]} - elif origin is dict: - out = {"type": "object"} - if len(args) == 2: - out["additionalProperties"] = _parse_type_hint(args[1]) - return out - raise TypeHintParsingException("Couldn't parse this type hint: ", hint) - - -_BASE_TYPE_MAPPING = { - int: {"type": "integer"}, float: {"type": "number"}, str: {"type": "string"}, - bool: {"type": "boolean"}, Any: {"type": "any"}, types.NoneType: {"type": "null"}, -} - -def _get_json_schema_type(param_type: str) -> Dict[str, str]: - if param_type in _BASE_TYPE_MAPPING: - return copy(_BASE_TYPE_MAPPING[param_type]) diff --git a/veriact/agent/__init__.py b/veriact/agent/__init__.py new file mode 100644 index 0000000..3c000e4 --- /dev/null +++ b/veriact/agent/__init__.py @@ -0,0 +1,6 @@ +"""Agent loop: VeriActAgent (entry point) + CLIAgent (ReAct-over-CLI loop).""" + +from veriact.agent.agent import VeriActAgent +from veriact.agent.cli_agent import CLIAgent + +__all__ = ["VeriActAgent", "CLIAgent"] diff --git a/veriact/agent/agent.py b/veriact/agent/agent.py index e5c5403..cc9c787 100644 --- a/veriact/agent/agent.py +++ b/veriact/agent/agent.py @@ -1,95 +1,135 @@ -"""VeriActAgent: CODEACT mode entry point.""" +"""VeriActAgent — CLI-ReAct entry point (drop-in replacement for VeriActAgent). + +Per task it materializes a small workspace (Solution.java placeholder, Test.java, +harness/task.json), runs the CLIAgent ReAct loop (which drives the tool CLI as +subprocesses), and records the same trajectory / memory / monitoring artifacts as +the original VeriAct. +""" from __future__ import annotations + import json import logging import os from datetime import datetime -from veriact.codeact import CodeAgent -from veriact.default_tools import TaskCompletionTool -from veriact.data_types import Task, HARNESS_PASS_THRESHOLD -from veriact.file_utility import dump_json -from veriact.memory import ActionStep -from veriact.tools import get_veriact_tools -from veriact.utility import AgentMaxStepsError +from veriact.agent.cli_agent import CLIAgent +from veriact.core.data_types import HARNESS_PASS_THRESHOLD, Task +from veriact.core.file_utility import dump_json +from veriact.core.memory import ActionStep +from veriact.tools.descriptors import RunHarnessTool, VerifyTool +from veriact.core.utility import AgentMaxStepsError logger = logging.getLogger(__name__) -class VeriActAgent: - """Verification-Guided Agentic Framework for Formal Specification Synthesis. +def _task_to_record(task: Task) -> dict: + """Serialize a Task to the dict shape harness_tool.Task.from_dict expects.""" + return { + "task_id": task.task_id, + "code": task.code, + "class_name": task.class_name, + "test_name": task.test_name, + "javadoc": task.javadoc, + "category": task.category, + "origin_id": task.origin_id, + "test_code": task.test_code, + "test_inputs": [{"input": tc.input, "output": tc.output} for tc in task.test_inputs], + "generated_test_cases": [ + {"input": tc.input, "output": tc.output} for tc in task.generated_test_cases + ], + } - Args: - model: Any veriact Model (OpenAIServerModel, AnthropicModel, GeminiModel, VLLMModel). - openjml_path: Path to OpenJML binary. - dataset_path: Path to the dataset used by the harness/retrieval tools. - output_dir: Directory for outputs. - """ + +class VeriActAgent: + """CLI-driven verification-guided spec synthesis agent.""" def __init__( self, model, openjml_path="openjml", - dataset_path="../benchmarks/example/data.json", + dataset_path="", output_dir="veriact_outputs", planning_interval=5, max_steps=15, harness_threshold=HARNESS_PASS_THRESHOLD, + no_harness: bool = False, _run_dir: str | None = None, **kwargs, ): self.model = model + self.openjml_path = openjml_path + self.dataset_path = dataset_path + self.max_steps = max_steps + self.planning_interval = planning_interval + self.harness_threshold = harness_threshold + self.no_harness = no_harness + self._kwargs = kwargs + if _run_dir: - # Use a pre-computed run directory (e.g. from batch mode) self.output_dir = _run_dir else: model_id = getattr(model, "model_id", "unknown") or "unknown" safe_model_id = model_id.replace("/", "_") timestamp = datetime.now().strftime("%Y%m%d_%H%M%S") - self.output_dir = os.path.join(output_dir, f"veriact__{safe_model_id}__{timestamp}") + self.output_dir = os.path.join( + output_dir, f"veriact__{safe_model_id}__{timestamp}" + ) os.makedirs(self.output_dir, exist_ok=True) - self._tools = get_veriact_tools( - openjml_path=openjml_path, - dataset_path=dataset_path, - output_dir=self.output_dir, - ) - self._codeact_kwargs = { - "planning_interval": planning_interval, - "max_steps": max_steps, - "harness_threshold": harness_threshold, - **kwargs, - } + def _setup_workspace(self, task: Task) -> tuple[str, str]: + safe_id = task.task_id.replace("/", "_").replace("\\", "_") + ws = os.path.join(self.output_dir, "workspaces", safe_id) + os.makedirs(os.path.join(ws, "harness"), exist_ok=True) + # Test.java for the agent / harness; Solution.java seeded with the bare code. + with open(os.path.join(ws, "Test.java"), "w") as fh: + fh.write(task.test_code or "") + with open(os.path.join(ws, "Solution.java"), "w") as fh: + fh.write(task.code or "") + task_json = os.path.join(ws, "harness", "task.json") + with open(task_json, "w") as fh: + json.dump(_task_to_record(task), fh, indent=2) + return ws, task_json def run(self, task: Task) -> dict: - agent = CodeAgent( - tools=self._tools + [TaskCompletionTool()], + workspace, task_json = self._setup_workspace(task) + + # Ablation: no-harness arm exposes only verify (+ task_complete) and uses + # the harness-free prompt; success = verification passes. + tools = [VerifyTool()] if self.no_harness else [VerifyTool(), RunHarnessTool()] + prompt_name = ( + "veriact_cli_no_harness_prompt.yaml" + if self.no_harness + else "veriact_cli_prompt.yaml" + ) + agent = CLIAgent( + tools=tools, model=self.model, - **self._codeact_kwargs, + task_id=task.task_id, + workspace_dir=workspace, + task_json=task_json, + openjml_path=self.openjml_path, + max_steps=self.max_steps, + planning_interval=self.planning_interval, + harness_threshold=self.harness_threshold, + prompt_name=prompt_name, + **self._kwargs, ) - task_str = f"task_id: {task.task_id}\n\n" f"java_code:\n{task.code}\n\n" + task_str = f"task_id: {task.task_id}\n\njava_code:\n{task.code}\n\n" result = agent.run(task=task_str) - _last_attempted_code = agent.get_last_jml_code() + last_code = agent.get_last_jml_code() - # Determine success: True only if the agent called task_complete - # voluntarily (not forced by hitting max_steps) AND the last - # run_spec_harness scores met the threshold. action_steps = [ - s - for s in agent.memory.steps + s for s in agent.memory.steps if isinstance(s, ActionStep) and s.step_number is not None ] - hit_max_steps = any( - isinstance(s.error, AgentMaxStepsError) for s in action_steps - ) - harness_passed = self._check_harness_passed( - action_steps, self._codeact_kwargs.get("harness_threshold", HARNESS_PASS_THRESHOLD) - ) - success = result is not None and not hit_max_steps and harness_passed - - # Count only real agent steps (exclude the forced max-steps step) + hit_max_steps = any(isinstance(s.error, AgentMaxStepsError) for s in action_steps) + if self.no_harness: + passed = self._check_verified(action_steps) + else: + passed = self._check_harness_passed(action_steps, self.harness_threshold) + success = result is not None and not hit_max_steps and passed iterations = sum( 1 for s in action_steps if not isinstance(s.error, AgentMaxStepsError) ) @@ -100,7 +140,7 @@ def run(self, task: Task) -> dict: "iterations": iterations, "agent_output": result, "agent_dict": agent.to_dict(), - "_last_attempted_code": _last_attempted_code, + "_last_attempted_code": last_code, } trajectories_dir = os.path.join(self.output_dir, "trajectories") @@ -109,37 +149,51 @@ def run(self, task: Task) -> dict: trajectory, os.path.join(trajectories_dir, f"{task.task_id}_veriact_trajectory.json"), ) - return trajectory @staticmethod def _check_harness_passed(action_steps: list[ActionStep], threshold: float) -> bool: - """Return True if the last run_spec_harness call met the threshold.""" + """True if the last run_spec_harness call met the threshold.""" for step in reversed(action_steps): for tool_out in reversed(step.tool_outputs or []): if tool_out.get("tool_name") != "run_spec_harness": continue - # Parse the harness output (JSON string with scores) raw = tool_out.get("output", "") try: scores = json.loads(raw) if isinstance(raw, str) else raw except (json.JSONDecodeError, TypeError): continue - # scores is {task_id: {metric: value, ...}} if isinstance(scores, dict): for _tid, metrics in scores.items(): if not isinstance(metrics, dict): continue pc = metrics.get("post_correctness", 0.0) pcm = metrics.get("post_completeness", 0.0) - if pc >= threshold and pcm >= threshold: - return True - return False # found last harness call but didn't pass - return False # no harness call found + return pc >= threshold and pcm >= threshold + return False + + @staticmethod + def _check_verified(action_steps: list[ActionStep]) -> bool: + """No-harness success: True if the last verify call reported verified=True.""" + for step in reversed(action_steps): + for tool_out in reversed(step.tool_outputs or []): + if tool_out.get("tool_name") != "verify": + continue + raw = tool_out.get("output", "") + try: + data = json.loads(raw) if isinstance(raw, str) else raw + except (json.JSONDecodeError, TypeError): + continue + if isinstance(data, dict): + return bool(data.get("verified")) + return False def to_dict(self): + tools = ["verify", "task_complete"] if self.no_harness else [ + "verify", "run_spec_harness", "task_complete" + ] return { - "mode": "codeact", + "mode": "cli-react" + ("-no-harness" if self.no_harness else ""), "model_id": getattr(self.model, "model_id", "?"), - "tools": [t.name for t in self._tools], + "tools": tools, } diff --git a/veriact/agent/cli_agent.py b/veriact/agent/cli_agent.py new file mode 100644 index 0000000..02f5f35 --- /dev/null +++ b/veriact/agent/cli_agent.py @@ -0,0 +1,582 @@ +"""CLI-ReAct agent — think -> run a CLI tool -> observe its stdout -> repeat. + +Replaces VeriAct's CodeAct (Python-code execution) with command-line tool calls. +At each step the model emits a JSON object ``{"thought", "tool", "tool_input"}``; +the agent runs the corresponding subcommand of [cli.py] as a **subprocess** and +feeds the CLI's JSON stdout back as the observation. Memory, monitoring, planning, +and trajectory recording are inherited unchanged from ``MultiStepAgent``. +""" + +from __future__ import annotations + +import importlib.resources +import inspect +import json +import os +import subprocess +import sys +import time +from collections import deque +from logging import getLogger +from typing import Any, Dict, Generator, Optional, TypedDict + +import yaml +from jinja2 import StrictUndefined, Template +from rich.console import Group +from rich.text import Text + +from veriact.core.agent_types import AgentType, handle_agent_output_types +from veriact.tools.default_tools import TaskCompletionTool +from veriact.core.memory import ( + ActionStep, + AgentMemory, + PlanningStep, + SystemPromptStep, + TaskCompleteStep, + TaskStep, + ToolCall, +) +from veriact.core.models import MessageRole +from veriact.core.monitoring import GREEN_HEX, AgentLogger, LogLevel, Monitor +from veriact.tools.base import Tool +from veriact.core.utility import ( + AgentError, + AgentExecutionError, + AgentGenerationError, + AgentMaxStepsError, + AgentParsingError, + is_valid_name, + make_json_serializable, + truncate_content, +) + +logger = getLogger(__name__) + +# Path to the tool CLI invoked as a subprocess (veriact/tools/cli.py). +_PKG_DIR = os.path.dirname(os.path.dirname(os.path.abspath(__file__))) # veriact/ +CLI_PATH = os.path.join(_PKG_DIR, "tools", "cli.py") + +def populate_template(template: str, variables: Dict[str, Any]) -> str: + return Template(template, undefined=StrictUndefined).render(**variables) + + +class PlanningPromptTemplate(TypedDict): + initial_plan: str + update_plan_pre_messages: str + update_plan_post_messages: str + + +class TaskCompletePromptTemplate(TypedDict): + pre_messages: str + post_messages: str + + +class PromptTemplates(TypedDict): + system_prompt: str + planning: PlanningPromptTemplate + task_complete: TaskCompletePromptTemplate + + +EMPTY_PROMPT_TEMPLATES = PromptTemplates( + system_prompt="", + planning=PlanningPromptTemplate( + initial_plan="", + update_plan_pre_messages="", + update_plan_post_messages="", + ), + task_complete=TaskCompletePromptTemplate(pre_messages="", post_messages=""), +) + + +# ============================================================ +# MultiStepAgent — generic ReAct loop (memory / monitoring / planning) +# ============================================================ + +class MultiStepAgent: + """ReAct-style agent: think -> act -> observe -> repeat.""" + + def __init__( + self, + tools, + model, + prompt_templates=None, + max_steps=15, + verbosity_level=LogLevel.INFO, + grammar=None, + step_callbacks=None, + planning_interval=None, + name=None, + description=None, + task_complete_checks=None, + harness_threshold=0.5, + ): + self.agent_name = self.__class__.__name__ + self.model = model + self.prompt_templates = prompt_templates or EMPTY_PROMPT_TEMPLATES + self.max_steps = max_steps + self.step_number = 0 + self.grammar = grammar + self.planning_interval = planning_interval + self.state = {} + self.name = name if (name is None or is_valid_name(name)) else None + self.description = description + self.task_complete_checks = task_complete_checks + self.harness_threshold = harness_threshold + + assert all(isinstance(t, Tool) for t in tools) + self.tools = {t.name: t for t in tools} + self.tools.setdefault("task_complete", TaskCompletionTool()) + + self.task = None + self.system_prompt = self.initialize_system_prompt() + self.memory = AgentMemory(self.system_prompt) + self.logger = AgentLogger(level=verbosity_level) + self.monitor = Monitor(self.model, self.logger) + self.step_callbacks = list(step_callbacks or []) + self.step_callbacks.append(self.monitor.update_metrics) + + def run(self, task, stream=False, reset=True, additional_args=None, max_steps=None): + max_steps = max_steps or self.max_steps + self.task = task + self.interrupt_switch = False + if additional_args: + self.state.update(additional_args) + self.task += f"\nAdditional args: {additional_args}" + + self.system_prompt = self.initialize_system_prompt(task=self.task) + self.memory.system_prompt = SystemPromptStep(system_prompt=self.system_prompt) + if reset: + self.memory.reset() + self.monitor.reset() + + self.logger.log_task( + content=self.task.strip(), + subtitle=f"{type(self.model).__name__} - {getattr(self.model, 'model_id', '')}", + level=LogLevel.INFO, + title=getattr(self, "name", None), + ) + self.memory.steps.append(TaskStep(task=self.task)) + + if stream: + return self._run(task=self.task, max_steps=max_steps) + return deque(self._run(task=self.task, max_steps=max_steps), maxlen=1)[0].task_complete + + def _run(self, task, max_steps) -> Generator[ActionStep | AgentType, None, None]: + task_complete = None + self.step_number = 1 + step_start_time = time.time() + while task_complete is None and self.step_number <= max_steps: + if self.interrupt_switch: + raise AgentError("Agent interrupted.", self.logger) + step_start_time = time.time() + if self.planning_interval and ( + self.step_number == 1 + or (self.step_number - 1) % self.planning_interval == 0 + ): + ps = self._create_planning_step( + task, is_first_step=(self.step_number == 1), step=self.step_number + ) + self.memory.steps.append(ps) + yield ps + action_step = ActionStep( + step_number=self.step_number, start_time=step_start_time + ) + try: + task_complete = self._execute_step(task, action_step) + except AgentGenerationError: + raise + except AgentError as e: + action_step.error = e + finally: + action_step.end_time = time.time() + action_step.duration = action_step.end_time - step_start_time + for cb in self.step_callbacks: + ( + cb(action_step) + if len(inspect.signature(cb).parameters) == 1 + else cb(action_step, agent=self) + ) + self.memory.steps.append(action_step) + yield action_step + self.step_number += 1 + + if task_complete is None and self.step_number == max_steps + 1: + task_complete = self.provide_task_complete(task) + final = ActionStep( + step_number=self.step_number, + error=AgentMaxStepsError("Reached max steps.", self.logger), + ) + final.action_output = task_complete + final.end_time = time.time() + final.duration = final.end_time - step_start_time + self.memory.steps.append(final) + for cb in self.step_callbacks: + ( + cb(final) + if len(inspect.signature(cb).parameters) == 1 + else cb(final, agent=self) + ) + yield final + yield TaskCompleteStep(task_complete=handle_agent_output_types(task_complete)) + + def _execute_step(self, task, memory_step): + self.logger.log_rule(f"Step {self.step_number}", level=LogLevel.INFO) + tc = self.step(memory_step) + if tc is not None and self.task_complete_checks: + for check in self.task_complete_checks: + try: + assert check(tc, self.memory) + except Exception as e: + raise AgentError(f"Check {check.__name__} failed: {e}", self.logger) + return tc + + def _create_planning_step(self, task, is_first_step, step): + if is_first_step: + input_messages = [ + { + "role": MessageRole.USER, + "content": [ + { + "type": "text", + "text": populate_template( + self.prompt_templates["planning"]["initial_plan"], + variables={"task": task, "tools": self.tools}, + ), + } + ], + } + ] + plan_message = self.model(input_messages, stop_sequences=[""]) + plan = f"Here are the facts and plan:\n```\n{plan_message.content}\n```" + else: + memory_messages = self.write_memory_to_messages(summary_mode=True) + pre = { + "role": MessageRole.SYSTEM, + "content": [ + { + "type": "text", + "text": populate_template( + self.prompt_templates["planning"]["update_plan_pre_messages"], + variables={"task": task}, + ), + } + ], + } + post = { + "role": MessageRole.USER, + "content": [ + { + "type": "text", + "text": populate_template( + self.prompt_templates["planning"]["update_plan_post_messages"], + variables={ + "task": task, + "tools": self.tools, + "remaining_steps": self.max_steps - step, + }, + ), + } + ], + } + input_messages = [pre] + memory_messages + [post] + plan_message = self.model(input_messages, stop_sequences=[""]) + plan = f"Updated plan:\n```\n{plan_message.content}\n```" + + return PlanningStep( + model_input_messages=input_messages, + plan=plan, + model_output_message=plan_message, + ) + + def initialize_system_prompt(self, task=None): + if self.prompt_templates.get("system_prompt"): + task_value = task if task is not None else getattr(self, "task", "") + return populate_template( + self.prompt_templates["system_prompt"], + variables={ + "tools": self.tools, + "task": task_value, + "harness_threshold": self.harness_threshold, + }, + ) + return "" + + def write_memory_to_messages(self, summary_mode=False): + messages = self.memory.system_prompt.to_messages(summary_mode=summary_mode) + for step in self.memory.steps: + messages.extend(step.to_messages(summary_mode=summary_mode)) + return messages + + def provide_task_complete(self, task): + pre = self.prompt_templates.get("task_complete", {}).get("pre_messages", "") + messages = self.write_memory_to_messages(summary_mode=True) + if pre: + messages = [ + {"role": MessageRole.SYSTEM, "content": [{"type": "text", "text": pre}]} + ] + messages + try: + return self.model(messages).content + except Exception as e: + return f"Error generating final output: {e}" + + def step(self, memory_step): + raise NotImplementedError + + def interrupt(self): + self.interrupt_switch = True + + def to_dict(self): + return { + "provided_tools": [t.name for t in self.tools.values()], + "model": { + "class": self.model.__class__.__name__, + "data": self.model.to_dict(), + }, + "prompt_templates": self.prompt_templates, + "max_steps": self.max_steps, + "planning_interval": self.planning_interval, + "name": self.name, + "description": self.description, + } + + +# ============================================================ +# CLIAgent — emits {thought, tool, tool_input}; runs the tool CLI as a subprocess +# ============================================================ + +class CLIAgent(MultiStepAgent): + """Agent that drives the verify / run_spec_harness / task_complete CLI tools.""" + + def __init__( + self, + tools, + model, + task_id: str, + workspace_dir: str, + task_json: str, + openjml_path: str = "openjml", + cli_path: str = CLI_PATH, + tool_timeout: int = 600, + prompt_templates=None, + prompt_name: str = "veriact_cli_prompt.yaml", + planning_interval=None, + harness_threshold=0.5, + **kwargs, + ): + if prompt_templates is None: + try: + prompt_templates = yaml.safe_load( + importlib.resources.files("veriact.prompts") + .joinpath(prompt_name) + .read_text() + ) + except Exception: + prompt_templates = EMPTY_PROMPT_TEMPLATES + + self.task_id = task_id + self.workspace_dir = workspace_dir + self.task_json = task_json + self.openjml_path = openjml_path + self.cli_path = cli_path + self.tool_timeout = tool_timeout + self._last_code: Optional[str] = None + self._solution_path = os.path.join(workspace_dir, "Solution.java") + + super().__init__( + tools=tools, + model=model, + prompt_templates=prompt_templates, + planning_interval=planning_interval, + harness_threshold=harness_threshold, + **kwargs, + ) + + # ---- response parsing --------------------------------------------- + + @staticmethod + def _parse_json_response(text: str) -> dict: + text = text.strip() + start = text.find("{") + if start == -1: + raise ValueError("No JSON object found in response") + obj, _ = json.JSONDecoder().raw_decode(text, start) + if not isinstance(obj, dict): + raise ValueError(f"Expected a JSON object, got {type(obj).__name__}") + return obj + + # ---- CLI tool execution ------------------------------------------- + + def _run_cli(self, cmd: list[str]) -> str: + try: + proc = subprocess.run( + cmd, capture_output=True, text=True, timeout=self.tool_timeout + ) + out = (proc.stdout or "").strip() + return out if out else (proc.stderr or "").strip() + except subprocess.TimeoutExpired: + return json.dumps({"error": "tool timed out", "timeout": self.tool_timeout}) + except Exception as e: # noqa: BLE001 + return json.dumps({"error": f"tool execution failed: {e}"}) + + def _execute_tool(self, tool_name: str, tool_input: dict) -> tuple[str, bool, dict]: + """Run a tool as a CLI subprocess. Returns (observation, is_complete, record).""" + # Reject tools not provided to this agent (e.g. run_spec_harness in the + # no-harness ablation arm) so the model is told to use an available one. + if tool_name not in self.tools: + available = ", ".join(self.tools.keys()) + obs = json.dumps( + {"error": f"tool '{tool_name}' is not available", "available_tools": available} + ) + return obs, False, {"tool_name": tool_name, "args": tool_input, "output": obs} + + if tool_name == "task_complete": + summary = tool_input.get("summary") or tool_input.get("answer") or "" + out_path = os.path.join(self.workspace_dir, "submission.json") + cmd = [sys.executable, self.cli_path, "submit", summary, "--out", out_path] + if self._last_code is not None: + cmd += ["--code", self._solution_path] + observation = self._run_cli(cmd) + return observation, True, { + "tool_name": "task_complete", + "args": {"summary": summary}, + "output": summary, + } + + code = tool_input.get("jml_annotated_code", "") + if not code: + obs = json.dumps({"error": "tool_input.jml_annotated_code is required"}) + return obs, False, {"tool_name": tool_name, "args": tool_input, "output": obs} + # persist the latest code so verify/harness read the same file + with open(self._solution_path, "w") as fh: + fh.write(code) + self._last_code = code + + if tool_name == "verify": + cmd = [ + sys.executable, self.cli_path, "verify", + "--code", self._solution_path, + "--openjml", self.openjml_path, + "--output-dir", os.path.join(self.workspace_dir, "tmp"), + ] + elif tool_name == "run_spec_harness": + cmd = [ + sys.executable, self.cli_path, "harness", + "--code", self._solution_path, + "--task-json", self.task_json, + "--openjml", self.openjml_path, + "--output-dir", os.path.join(self.workspace_dir, "harness"), + "--run-id", f"step_{self.step_number}", + ] + else: + obs = json.dumps({"error": f"unknown tool '{tool_name}'"}) + return obs, False, {"tool_name": tool_name, "args": tool_input, "output": obs} + + observation = self._run_cli(cmd) + return observation, False, { + "tool_name": tool_name, + "args": {"task_id": self.task_id}, + "output": observation, + } + + # ---- one ReAct step ----------------------------------------------- + + def step(self, memory_step): + memory_messages = self.write_memory_to_messages() + memory_step.model_input_messages = memory_messages.copy() + # No response_format / function-calling: the model emits the JSON object + # described in the system prompt; we parse it and invoke the CLI ourselves. + try: + chat_message = self.model( + memory_messages, + stop_sequences=["observation:"], + ) + memory_step.model_output_message = chat_message + memory_step.model_output = chat_message.content + except Exception as e: + raise AgentGenerationError(f"Error generating model output:\n{e}", self.logger) from e + + self.logger.log_markdown( + content=memory_step.model_output or "", title="LLM Output:", level=LogLevel.DEBUG + ) + + try: + parsed = self._parse_json_response(memory_step.model_output) + tool_name = parsed["tool"] + tool_input = parsed.get("tool_input", {}) or {} + memory_step.thought = parsed.get("thought", "") + except Exception as e: + raise AgentParsingError( + f"Error parsing action:\n{e}\nRaw output:\n{(memory_step.model_output or '')[:500]}", + self.logger, + ) + + # record the JML code for trajectory / last-code retrieval + memory_step.code_action = tool_input.get("jml_annotated_code", "") or memory_step.code_action + memory_step.tool_calls = [ + ToolCall( + name=tool_name, + arguments=tool_input, + id=f"call_{len(self.memory.steps)}", + ) + ] + self.logger.log( + Text(f"-> {tool_name}({', '.join(tool_input.keys())})"), level=LogLevel.INFO + ) + + try: + observation, is_complete, record = self._execute_tool(tool_name, tool_input) + memory_step.is_action_executed = True + except Exception as e: + memory_step.is_action_executed = False + raise AgentExecutionError(str(e), self.logger) + + memory_step.observations = truncate_content(observation) + memory_step.tool_outputs = [record] + memory_step.action_output = observation + + self.logger.log( + Group( + Text( + f"{'Task Completed - ' if is_complete else 'Observation'}:\n{memory_step.observations}", + style=f"bold {GREEN_HEX}" if is_complete else "", + ) + ), + level=LogLevel.INFO, + ) + return observation if is_complete else None + + # ---- helpers used by the wrapper ---------------------------------- + + def get_last_jml_code(self) -> Optional[str]: + return self._last_code + + def to_dict(self): + d = super().to_dict() + d["trajectories"] = self._generate_trajectory() + return d + + def _generate_trajectory(self): + task_steps = [s for s in self.memory.steps if isinstance(s, TaskStep)] + planning_steps = [s for s in self.memory.steps if isinstance(s, PlanningStep)] + action_steps = [s for s in self.memory.steps if isinstance(s, ActionStep)] + steps = [] + for step in action_steps: + tool_calls = step.tool_calls or [] + invoked = [tc.name for tc in tool_calls] + steps.append( + { + "step_no": step.step_number, + "thought": step.thought, + "tool_calls": [tc.dict() for tc in tool_calls], + "code": step.code_action, + "observations": step.observations, + "tool_outputs": make_json_serializable(step.tool_outputs or []), + "invoked_tools": invoked, + "is_tool_executed": step.is_action_executed, + } + ) + return { + "task": [t.task for t in task_steps if t.task], + "plan": [p.plan for p in planning_steps if p.plan], + "steps": steps, + } diff --git a/veriact/codeact.py b/veriact/codeact.py deleted file mode 100644 index 59504f5..0000000 --- a/veriact/codeact.py +++ /dev/null @@ -1,821 +0,0 @@ -"""MultiStepAgent and CodeAgent — ReAct-style agentic loop with code execution.""" - -import ast -import builtins -import contextlib -import importlib -import inspect -import io -import json -import textwrap -import time -import traceback -from collections import deque -from logging import getLogger -from typing import ( - Any, - Dict, - Generator, - Optional, - TypedDict, -) - -import yaml -from jinja2 import StrictUndefined, Template -from rich.console import Group -from rich.rule import Rule -from rich.text import Text - -from veriact.agent_types import AgentType, handle_agent_output_types -from veriact.default_tools import TaskCompletionTool -from veriact.memory import ( - ActionStep, - AgentMemory, - PlanningStep, - SystemPromptStep, - TaskCompleteStep, - TaskStep, - ToolCall, -) -from veriact.models import ChatMessage, MessageRole -from veriact.monitoring import GREEN_HEX, AgentLogger, LogLevel, Monitor -from veriact.tools_base import Tool -from veriact.utility import ( - CODEAGENT_RESPONSE_FORMAT, - AgentError, - AgentExecutionError, - AgentGenerationError, - AgentMaxStepsError, - AgentParsingError, - extract_code_from_text, - is_valid_name, - make_json_serializable, - truncate_content, - find_tool_usage, -) - -logger = getLogger(__name__) - - -# In-process execution guards - - -class _TaskCompleteSignal(Exception): - """Raised by the injected task_complete() to cleanly signal run completion.""" - - def __init__(self, result=None): - self.result = result - - -# Top-level module names that agent code must not import -_BLOCKED_IMPORTS = frozenset( - { - "subprocess", - "socket", - "requests", - "urllib", - "http", - "ftplib", - "smtplib", - "telnetlib", - "xmlrpc", - "paramiko", - "fabric", - "multiprocessing", - "ctypes", - "cffi", - "pty", - "pexpect", - "importlib", - } -) - -# os.* calls that could escape the process -_BLOCKED_OS_CALLS = frozenset( - { - "system", - "popen", - "execv", - "execve", - "execvp", - "execvpe", - "execl", - "execle", - "execlp", - "execlpe", - "spawn", - "spawnl", - "spawnle", - "spawnlp", - "spawnlpe", - "spawnv", - "spawnve", - "spawnvp", - "spawnvpe", - "fork", - "forkpty", - "kill", - "killpg", - "remove", - "unlink", - "rmdir", - "removedirs", - "chmod", - "chown", - "setuid", - "setgid", - } -) - -# Builtin calls blocked in agent code -_BLOCKED_BUILTINS = frozenset({"eval", "exec", "compile", "__import__", "breakpoint"}) - - -class _CodeSafetyChecker(ast.NodeVisitor): - """AST visitor that collects dangerous code patterns before execution.""" - - def __init__(self): - self.violations: list[str] = [] - - def visit_Import(self, node: ast.Import): - for alias in node.names: - if alias.name.split(".")[0] in _BLOCKED_IMPORTS: - self.violations.append(f"Blocked import: '{alias.name}'") - self.generic_visit(node) - - def visit_ImportFrom(self, node: ast.ImportFrom): - if node.module and node.module.split(".")[0] in _BLOCKED_IMPORTS: - self.violations.append(f"Blocked import: 'from {node.module} import ...'") - self.generic_visit(node) - - def visit_Call(self, node: ast.Call): - if isinstance(node.func, ast.Name) and node.func.id in _BLOCKED_BUILTINS: - self.violations.append(f"Blocked builtin: '{node.func.id}()'") - elif isinstance(node.func, ast.Attribute): - obj, attr = node.func.value, node.func.attr - if isinstance(obj, ast.Name): - if obj.id == "os" and attr in _BLOCKED_OS_CALLS: - self.violations.append(f"Blocked OS call: 'os.{attr}()'") - elif obj.id == "subprocess": - self.violations.append(f"Blocked call: 'subprocess.{attr}()'") - self.generic_visit(node) - - def visit_Attribute(self, node: ast.Attribute): - # Block common sandbox-escape paths via class hierarchy traversal - if node.attr in { - "__subclasses__", - "__globals__", - "__builtins__", - "__code__", - "__closure__", - }: - self.violations.append(f"Blocked attribute access: '.{node.attr}'") - self.generic_visit(node) - - -def populate_template(template: str, variables: Dict[str, Any]) -> str: - return Template(template, undefined=StrictUndefined).render(**variables) - - -class PlanningPromptTemplate(TypedDict): - initial_facts: str - initial_plan: str - update_facts_pre_messages: str - update_facts_post_messages: str - update_plan_pre_messages: str - update_plan_post_messages: str - - -class TaskCompletePromptTemplate(TypedDict): - pre_messages: str - post_messages: str - - -class PromptTemplates(TypedDict): - system_prompt: str - planning: PlanningPromptTemplate - task_complete: TaskCompletePromptTemplate - - -EMPTY_PROMPT_TEMPLATES = PromptTemplates( - system_prompt="", - planning=PlanningPromptTemplate( - initial_facts="", - initial_plan="", - update_facts_pre_messages="", - update_facts_post_messages="", - update_plan_pre_messages="", - update_plan_post_messages="", - ), - task_complete=TaskCompletePromptTemplate(pre_messages="", post_messages=""), -) - - -class MultiStepAgent: - """ReAct-style agent: think → act → observe → repeat.""" - - def __init__( - self, - tools, - model, - prompt_templates=None, - max_steps=5, - verbosity_level=LogLevel.INFO, - grammar=None, - step_callbacks=None, - planning_interval=None, - name=None, - description=None, - provide_run_summary=False, - task_complete_checks=None, - harness_threshold=0.5, - ): - self.agent_name = self.__class__.__name__ - self.model = model - self.prompt_templates = prompt_templates or EMPTY_PROMPT_TEMPLATES - self.max_steps = max_steps - self.step_number = 0 - self.grammar = grammar - self.planning_interval = planning_interval - self.state = {} - self.name = name if (name is None or is_valid_name(name)) else None - self.description = description - self.provide_run_summary = provide_run_summary - self.task_complete_checks = task_complete_checks - self.harness_threshold = harness_threshold - - assert all(isinstance(t, Tool) for t in tools) - self.tools = {t.name: t for t in tools} - self.tools.setdefault("task_complete", TaskCompletionTool()) - - self.task = None - self.system_prompt = self.initialize_system_prompt() - self.memory = AgentMemory(self.system_prompt) - self.logger = AgentLogger(level=verbosity_level) - self.monitor = Monitor(self.model, self.logger) - self.step_callbacks = list(step_callbacks or []) - self.step_callbacks.append(self.monitor.update_metrics) - - def run(self, task, stream=False, reset=True, additional_args=None, max_steps=None): - max_steps = max_steps or self.max_steps - self.task = task - self.interrupt_switch = False - if additional_args: - self.state.update(additional_args) - self.task += f"\nAdditional args: {additional_args}" - - self.system_prompt = self.initialize_system_prompt(task=self.task) - self.memory.system_prompt = SystemPromptStep(system_prompt=self.system_prompt) - if reset: - self.memory.reset() - self.monitor.reset() - - self.logger.log_task( - content=self.task.strip(), - subtitle=f"{type(self.model).__name__} - {getattr(self.model, 'model_id', '')}", - level=LogLevel.INFO, - title=getattr(self, "name", None), - ) - self.memory.steps.append(TaskStep(task=self.task)) - - if stream: - return self._run(task=self.task, max_steps=max_steps) - return deque(self._run(task=self.task, max_steps=max_steps), maxlen=1)[ - 0 - ].task_complete - - def _run(self, task, max_steps) -> Generator[ActionStep | AgentType, None, None]: - task_complete = None - self.step_number = 1 - step_start_time = time.time() - while task_complete is None and self.step_number <= max_steps: - if self.interrupt_switch: - raise AgentError("Agent interrupted.", self.logger) - step_start_time = time.time() - if self.planning_interval and ( - self.step_number == 1 - or (self.step_number - 1) % self.planning_interval == 0 - ): - ps = self._create_planning_step( - task, is_first_step=(self.step_number == 1), step=self.step_number - ) - self.memory.steps.append(ps) - yield ps - action_step = ActionStep( - step_number=self.step_number, start_time=step_start_time - ) - try: - task_complete = self._execute_step(task, action_step) - except AgentGenerationError: - raise - except AgentError as e: - action_step.error = e - finally: - action_step.end_time = time.time() - action_step.duration = action_step.end_time - step_start_time - for cb in self.step_callbacks: - ( - cb(action_step) - if len(inspect.signature(cb).parameters) == 1 - else cb(action_step, agent=self) - ) - self.memory.steps.append(action_step) - yield action_step - self.step_number += 1 - - if task_complete is None and self.step_number == max_steps + 1: - task_complete = self.provide_task_complete(task) - final = ActionStep( - step_number=self.step_number, - error=AgentMaxStepsError("Reached max steps.", self.logger), - ) - final.action_output = task_complete - final.end_time = time.time() - final.duration = final.end_time - step_start_time - self.memory.steps.append(final) - for cb in self.step_callbacks: - ( - cb(final) - if len(inspect.signature(cb).parameters) == 1 - else cb(final, agent=self) - ) - yield final - yield TaskCompleteStep(task_complete=handle_agent_output_types(task_complete)) - - def _execute_step(self, task, memory_step): - self.logger.log_rule(f"Step {self.step_number}", level=LogLevel.INFO) - tc = self.step(memory_step) - if tc is not None and self.task_complete_checks: - for check in self.task_complete_checks: - try: - assert check(tc, self.memory) - except Exception as e: - raise AgentError(f"Check {check.__name__} failed: {e}", self.logger) - return tc - - def _create_planning_step(self, task, is_first_step, step): - if is_first_step: - input_messages = [ - { - "role": MessageRole.USER, - "content": [ - { - "type": "text", - "text": populate_template( - self.prompt_templates["planning"]["initial_plan"], - variables={"task": task, "tools": self.tools}, - ), - } - ], - } - ] - plan_message = self.model(input_messages, stop_sequences=[""]) - plan = f"Here are the facts and plan:\n```\n{plan_message.content}\n```" - else: - memory_messages = self.write_memory_to_messages(summary_mode=True) - pre = { - "role": MessageRole.SYSTEM, - "content": [ - { - "type": "text", - "text": populate_template( - self.prompt_templates["planning"][ - "update_plan_pre_messages" - ], - variables={"task": task}, - ), - } - ], - } - post = { - "role": MessageRole.USER, - "content": [ - { - "type": "text", - "text": populate_template( - self.prompt_templates["planning"][ - "update_plan_post_messages" - ], - variables={ - "task": task, - "tools": self.tools, - "remaining_steps": self.max_steps - step, - }, - ), - } - ], - } - input_messages = [pre] + memory_messages + [post] - plan_message = self.model(input_messages, stop_sequences=[""]) - plan = f"Updated plan:\n```\n{plan_message.content}\n```" - - self.logger.log( - Rule( - f"[bold]{'Initial' if is_first_step else 'Updated'} plan", - style="orange", - ), - Text(plan), - level=LogLevel.INFO, - ) - return PlanningStep( - model_input_messages=input_messages, - plan=plan, - model_output_message=plan_message, - ) - - def initialize_system_prompt(self, task=None): - if self.prompt_templates.get("system_prompt"): - task_value = task if task is not None else getattr(self, "task", "") - return populate_template( - self.prompt_templates["system_prompt"], - variables={ - "tools": self.tools, - "task": task_value, - "harness_threshold": self.harness_threshold, - }, - ) - return "" - - def write_memory_to_messages(self, summary_mode=False): - messages = self.memory.system_prompt.to_messages(summary_mode=summary_mode) - for step in self.memory.steps: - messages.extend(step.to_messages(summary_mode=summary_mode)) - return messages - - def provide_task_complete(self, task): - pre = self.prompt_templates.get("task_complete", {}).get("pre_messages", "") - messages = self.write_memory_to_messages(summary_mode=True) - if pre: - messages = [ - { - "role": MessageRole.SYSTEM, - "content": [{"type": "text", "text": pre}], - } - ] + messages - try: - return self.model(messages).content - except Exception as e: - return f"Error generating final output: {e}" - - def step(self, memory_step): - pass - - def interrupt(self): - self.interrupt_switch = True - - def visualize(self): - self.logger.visualize_agent_tree(self) - - def to_dict(self): - tool_dicts = [t.to_dict() for t in self.tools.values()] - return { - "provided_tools": [t["name"] for t in tool_dicts], - "model": { - "class": self.model.__class__.__name__, - "data": self.model.to_dict(), - }, - "prompt_templates": self.prompt_templates, - "max_steps": self.max_steps, - "planning_interval": self.planning_interval, - "name": self.name, - "description": self.description, - } - - -class CodeAgent(MultiStepAgent): - """Agent that generates Python code to call tools.""" - - def __init__( - self, - tools, - model, - prompt_templates=None, - grammar=None, - planning_interval=None, - code_block_tags=None, - executor_kwargs=None, - max_print_outputs_length=None, - harness_threshold=0.5, - **kwargs, - ): - self.max_print_outputs_length = max_print_outputs_length - - # Load default prompts if none provided - if prompt_templates is None: - try: - prompt_templates = yaml.safe_load( - importlib.resources.files("veriact.prompts") - .joinpath("veriact_prompt.yaml") - .read_text() - ) - except Exception: - prompt_templates = EMPTY_PROMPT_TEMPLATES - - self.code_block_tags = ( - code_block_tags - if isinstance(code_block_tags, tuple) - else ( - ("```python", "```") - if code_block_tags == "markdown" - else ("", "") - ) - ) - - super().__init__( - tools=tools, - model=model, - prompt_templates=prompt_templates, - grammar=grammar, - planning_interval=planning_interval, - harness_threshold=harness_threshold, - **kwargs, - ) - - self.executor_kwargs = executor_kwargs or {} - self._init_execution_namespace() - - @staticmethod - def _parse_json_response(text: str) -> dict: - """Parse the first JSON object from *text*, ignoring trailing content. - - Models like Claude may append extra text after the JSON object (e.g. - "Calling tools: …"). ``json.loads`` rejects that with "Extra data", - so we use ``json.JSONDecoder.raw_decode`` which stops after the first - valid JSON value. If the JSON doesn't start at position 0 we scan - for the first ``{``. - """ - text = text.strip() - decoder = json.JSONDecoder() - # Find the first '{' in case there's leading text - start = text.find("{") - if start == -1: - raise ValueError("No JSON object found in response") - obj, _ = decoder.raw_decode(text, start) - if not isinstance(obj, dict): - raise ValueError(f"Expected a JSON object, got {type(obj).__name__}") - return obj - - def _init_execution_namespace(self) -> None: - """Set up a fresh shared namespace for in-process code execution. - - Tool instances are injected directly by name so agent code can call - e.g. ``verify_with_openjml(...)`` without any import or serialisation. - The namespace persists across all steps in a single run, so variables - defined in step N are visible in step N+1. - """ - # Per-step list that accumulates {tool_name, args, output} dicts. - # Cleared at the start of each step in execute_code(). - self._current_tool_outputs: list[dict[str, Any]] = [] - - ns: dict[str, Any] = {} - for t in self.tools.values(): - if t.name == "task_complete": - continue - ns[t.name] = self._wrap_tool(t) - - # Wrap task_complete so calling it raises _TaskCompleteSignal, which - # execute_code catches to set is_task_complete=True. - _tc_tool = self.tools.get("task_complete") - - def _task_complete(summary: str = ""): - result = _tc_tool(summary=summary) if _tc_tool else summary - self._current_tool_outputs.append( - {"tool_name": "task_complete", "args": {"summary": summary}, "output": result} - ) - raise _TaskCompleteSignal(result) - - ns["task_complete"] = _task_complete - - # Defense-in-depth: strip the most dangerous builtins at runtime and - # replace __import__ with a guarded version (AST check is the primary - # guard; this catches anything that slips through at parse time). - _orig_import = builtins.__import__ - - def _guarded_import(name, globals_=None, locals_=None, fromlist=(), level=0): - if name.split(".")[0] in _BLOCKED_IMPORTS: - raise ImportError(f"Import of '{name}' is not permitted in agent code.") - return _orig_import(name, globals_, locals_, fromlist, level) - - safe_builtins = { - k: v - for k, v in vars(builtins).items() - if k not in {"eval", "exec", "compile", "breakpoint"} - } - safe_builtins["__import__"] = _guarded_import - ns["__builtins__"] = safe_builtins - - self.execution_namespace = ns - - def _wrap_tool(self, tool: Tool): - """Return a wrapper that delegates to *tool* but records its output. - - Stdout is suppressed during the tool call so that internal noise - (e.g. harness mutant-verification output) does not leak into the - agent's observations. Only the agent's own print() calls appear. - """ - def wrapper(*args, **kwargs): - # Suppress any stdout the tool produces internally so it - # doesn't pollute the agent's observation buffer. - with contextlib.redirect_stdout(io.StringIO()): - result = tool(*args, **kwargs) - self._current_tool_outputs.append( - {"tool_name": tool.name, "args": {"args": args, "kwargs": kwargs}, "output": result} - ) - return result - # Preserve the original tool's attributes for introspection - wrapper.__name__ = tool.name - wrapper.__doc__ = getattr(tool, "description", None) - return wrapper - - def _check_code_safety(self, code: str) -> list[str]: - """Return a list of safety violations; empty means the code is safe.""" - try: - tree = ast.parse(code) - except SyntaxError as e: - return [f"SyntaxError: {e}"] - checker = _CodeSafetyChecker() - checker.visit(tree) - return checker.violations - - def execute_code(self, code_action: str) -> tuple[str, int, bool]: - """Execute *code_action* in-process and return (output, error_code, is_task_complete).""" - self._current_tool_outputs = [] # reset per step - violations = self._check_code_safety(code_action) - if violations: - msg = "Code safety check failed:\n" + "\n".join( - f" - {v}" for v in violations - ) - return msg, 1, False - - buf = io.StringIO() - error_code = 0 - is_task_complete = False - try: - compiled = compile(code_action, "", "exec") - with contextlib.redirect_stdout(buf): - exec(compiled, self.execution_namespace) # noqa: S102 - except _TaskCompleteSignal: - is_task_complete = True - except Exception: - error_code = 1 - buf.write(traceback.format_exc()) - - return buf.getvalue(), error_code, is_task_complete - - def run(self, task, stream=False, reset=True, additional_args=None, max_steps=None): - if reset: - self._init_execution_namespace() - return super().run( - task, - stream=stream, - reset=reset, - additional_args=additional_args, - max_steps=max_steps, - ) - - def step(self, memory_step): - memory_messages = self.write_memory_to_messages() - memory_step.model_input_messages = memory_messages.copy() - _stop_sequences = ["observation:"] - if self.code_block_tags[1] not in self.code_block_tags[0]: - _stop_sequences.append(self.code_block_tags[1]) - - try: - additional_args: dict[str, Any] = {} - if self.grammar: - additional_args["grammar"] = self.grammar - additional_args["response_format"] = CODEAGENT_RESPONSE_FORMAT - chat_message = self.model( - memory_messages, stop_sequences=_stop_sequences, **additional_args - ) - memory_step.model_output_message = chat_message - output_text = chat_message.content - if output_text and not output_text.strip().endswith( - self.code_block_tags[1] - ): - memory_step.model_output_message.content = ( - output_text + self.code_block_tags[1] - ) - memory_step.model_output = output_text - except Exception as e: - raise AgentGenerationError( - f"Error generating model output:\n{e}", self.logger - ) from e - - self.logger.log_markdown( - content=output_text, title="LLM Output:", level=LogLevel.DEBUG - ) - - try: - parsed = self._parse_json_response(output_text) - code_action = parsed["code"] - code_action = ( - extract_code_from_text(code_action, self.code_block_tags) or code_action - ) - memory_step.code_action = code_action - memory_step.thought = parsed.get("thought", "") - except Exception as e: - raise AgentParsingError(f"Error parsing code:\n{e}\nRaw output:\n{output_text[:500]}", self.logger) - - memory_step.tool_calls = [ - ToolCall( - name="python_interpreter", - arguments=code_action, - id=f"call_{len(self.memory.steps)}", - ) - ] - - self.logger.log_code( - title="Executing:", content=code_action, level=LogLevel.INFO - ) - - output = "" - error_code = -1 - is_task_complete = False - execution_outputs_console = [] - try: - output, error_code, is_task_complete = self.execute_code(code_action) - if error_code == 0: - memory_step.is_action_executed = True - else: - memory_step.is_action_executed = False - except Exception as e: - if error_code != 0: - memory_step.observations = output - memory_step.is_action_executed = False - raise AgentExecutionError(str(e), self.logger) - - memory_step.observations = truncate_content(output) - memory_step.tool_outputs = list(self._current_tool_outputs) - - if is_task_complete: - self.logger.log(f"Task completed.", level=LogLevel.INFO) - - execution_outputs_console.append( - Text( - f"{'Task Completed - ' if is_task_complete else 'Out'}: \n{memory_step.observations}", - style=f"bold {GREEN_HEX}" if is_task_complete else "", - ) - ) - self.logger.log(Group(*execution_outputs_console), level=LogLevel.INFO) - memory_step.action_output = output - return output if is_task_complete else None - - def get_last_jml_code(self) -> Optional[str]: - """Extract the last JML-annotated Java code from the agent's execution namespace. - - Falls back to scanning action steps in reverse for code passed to - verify_with_openjml or run_spec_harness. - """ - # Primary: grab from the shared execution namespace - code = self.execution_namespace.get("code") - if code and isinstance(code, str) and "class" in code: - return code - - # Fallback: scan steps in reverse for the last tool invocation with JML code - import re - - action_steps = [ - s for s in self.memory.steps if isinstance(s, ActionStep) and s.code_action - ] - for step in reversed(action_steps): - src = step.code_action - if "verify_with_openjml" in src or "run_spec_harness" in src: - # Try to extract a triple-quoted Java string - match = re.search( - r"(?:r?'''(.*?)'''|r?\"\"\"(.*?)\"\"\")", src, re.DOTALL - ) - if match: - return match.group(1) or match.group(2) - return None - - def to_dict(self): - d = super().to_dict() - d["executor_kwargs"] = self.executor_kwargs - d["trajectories"] = self._generate_trajectory() - return d - - def _generate_trajectory(self): - tool_names = [t.name for t in self.tools.values()] - task_steps = [s for s in self.memory.steps if isinstance(s, TaskStep)] - planning_steps = [s for s in self.memory.steps if isinstance(s, PlanningStep)] - action_steps = [s for s in self.memory.steps if isinstance(s, ActionStep)] - steps = [] - for step in action_steps: - used = find_tool_usage(str(step.code_action), tool_names) - steps.append( - { - "step_no": step.step_number, - "thought": step.thought, - "code": step.code_action, - "observations": step.observations, - "tool_outputs": make_json_serializable(step.tool_outputs or []), - "invoked_tools": used, - "is_tool_executed": step.is_action_executed, - } - ) - return { - "task": [t.task for t in task_steps if t.task], - "plan": [p.plan for p in planning_steps if p.plan], - "steps": steps, - } diff --git a/veriact/config.py b/veriact/config.py index 7b7818a..601407a 100644 --- a/veriact/config.py +++ b/veriact/config.py @@ -1,5 +1,20 @@ +"""Load environment variables for veriact. + +Loads, in order: a .env discovered from the cwd upward, and the VeriAct repo's +``config/.env`` if present (so existing API keys keep working). Real environment +variables always take precedence. +""" + from pathlib import Path -from dotenv import load_dotenv -_BASE_DIR = Path(__file__).parent.parent # base directory of the project veriact -load_dotenv(dotenv_path=str(_BASE_DIR / "config" / ".env")) +from dotenv import find_dotenv, load_dotenv + +# 1) nearest .env from cwd upward (no error if missing) +load_dotenv(find_dotenv(usecwd=True)) + +# 2) repo config/.env relative to this package, if it exists +for base in (Path(__file__).resolve().parent, *Path(__file__).resolve().parents): + candidate = base / "config" / ".env" + if candidate.exists(): + load_dotenv(dotenv_path=str(candidate)) + break diff --git a/veriact/core/__init__.py b/veriact/core/__init__.py new file mode 100644 index 0000000..e69de29 diff --git a/veriact/core/memory.py b/veriact/core/memory.py index 8d14099..ecd06b6 100644 --- a/veriact/core/memory.py +++ b/veriact/core/memory.py @@ -6,9 +6,9 @@ from dataclasses import asdict, dataclass, field from typing import Any, Dict, List, Optional, TypedDict, Union -from veriact.models import ChatMessage, MessageRole -from veriact.monitoring import AgentLogger, LogLevel -from veriact.utility import AgentError, make_json_serializable +from veriact.core.models import ChatMessage, MessageRole +from veriact.core.monitoring import AgentLogger, LogLevel +from veriact.core.utility import AgentError, make_json_serializable logger = logging.getLogger(__name__) diff --git a/veriact/core/models.py b/veriact/core/models.py index 982499f..2fe28b5 100644 --- a/veriact/core/models.py +++ b/veriact/core/models.py @@ -12,8 +12,8 @@ from enum import Enum from typing import Any -from veriact.tools_base import Tool -from veriact.utility import _is_package_available, encode_image_base64, make_image_url, parse_json_blob +from veriact.tools.base import Tool +from veriact.core.utility import _is_package_available, encode_image_base64, make_image_url, parse_json_blob logger = logging.getLogger(__name__) diff --git a/veriact/core/monitoring.py b/veriact/core/monitoring.py index 4d1d367..2f6d997 100644 --- a/veriact/core/monitoring.py +++ b/veriact/core/monitoring.py @@ -13,7 +13,7 @@ from rich.text import Text from rich.tree import Tree from dataclasses import dataclass, field -from veriact.utility import escape_code_brackets +from veriact.core.utility import escape_code_brackets YELLOW_HEX = "#d4b702" BLUE_HEX = "#1E90FF" diff --git a/veriact/prompts/veriact_cli_no_harness_prompt.yaml b/veriact/prompts/veriact_cli_no_harness_prompt.yaml new file mode 100644 index 0000000..375fa6b --- /dev/null +++ b/veriact/prompts/veriact_cli_no_harness_prompt.yaml @@ -0,0 +1,138 @@ +system_prompt: |- + You are an expert Formal Verification Engineer. Given a Java program, synthesize JML specifications and iteratively verify them using OpenJML. + + You work in a thought -> tool -> observation loop. Each step you call ONE command-line tool and observe its JSON output. + + ## Output Format + + At each step, output exactly one JSON object — nothing else: + + {"thought": "your reasoning", "tool": "", "tool_input": { ... }} + + - "tool" must be one of: verify, task_complete. + - Provide the COMPLETE annotated Java source in tool_input each time you call verify. + - The class MUST be named Solution. + + ## Tools + + verify + tool_input: {"jml_annotated_code": ""} + Runs OpenJML ESC and returns the result WITH error analysis: + {"verified": bool, "return_code": int, "errors": [{"type","raw"}], + "failure_modes": [str], "repair_hints": [str], "summary": str, "raw_output": str} + Use at every verification attempt. Read repair_hints/summary to fix failures. + On Timeout (raw_output contains "Timeout"): STOP and simplify the spec before retrying. + NEVER resubmit the same or structurally identical spec after a timeout. + + task_complete + tool_input: {"summary": ""} + Mark the task complete. Call as soon as verification passes (verified=true). + + ## Workflow + + 1. Analyze the Java method and infer its behavior. + 2. Synthesize JML (requires, ensures, loop_invariant, assignable, decreases as needed). + Aim for a spec that is both correct (true for the method) and strong (captures the + full input/output relationship), not a trivially-true one. + 3. Call verify. + - verified=false -> read repair_hints/summary, refine the spec, go to 3. + - Timeout -> simplify spec (see Timeout Strategy), go to 3. + - verified=true -> call task_complete IMMEDIATELY. + + ## Timeout Strategy + + Timeout means the SMT prover ran out of time. The spec is too complex, not necessarily wrong. + On timeout: do NOT resubmit the same spec; simplify (split compound invariants, remove nested + quantifiers, weaken temporarily, use \old sparingly, tighten assignable, prefer \result == expr + over \exists). On repeated timeouts, simplify further. Never revert to a timed-out spec. + + ## Success criterion + + verify returns "verified": true. As soon as it does, submit your strongest verifying spec + with task_complete. There is NO spec-harness tool in this configuration. + + ## Example + + task_id = "maxElement_001" + + Step 1 - draft and verify: + {"thought": "maxElement returns the largest element. ensures result >= all elements and result is in the array.", "tool": "verify", "tool_input": {"jml_annotated_code": "public class Solution {\n /*@ requires arr != null && arr.length > 0;\n @ ensures (\\forall int i; 0 <= i && i < arr.length; arr[i] <= \\result);\n @ ensures (\\exists int i; 0 <= i && i < arr.length; arr[i] == \\result);\n @*/\n public static int maxElement(int[] arr) {\n int max = arr[0];\n for (int i = 1; i < arr.length; i++) { if (arr[i] > max) max = arr[i]; }\n return max;\n }\n}"}} + + Observation: {"verified": false, "failure_modes": ["PostconditionFailure"], "repair_hints": ["PostconditionFailure: ..."], "summary": "PostconditionFailure", "raw_output": "..."} + + Step 2 - add loop invariants and re-verify (tool=verify with the fixed code). + + Observation: {"verified": true, "return_code": 0, "errors": [], "summary": "No failures detected."} + + Step 3 - verification passed, complete: + {"thought": "verified=true. Submitting.", "tool": "task_complete", "tool_input": {"summary": "Verified JML for maxElement with loop invariants (requires non-empty array; ensures result is the maximum)."}} + + Note: task_id is provided in the task description. + + Now Begin! + + Task: + ``` + {{task}} + ``` + +planning: + initial_plan: |- + Analyze the Java program and plan your JML specification approach. + + ## Analysis + 1. What does the method do? (inputs, outputs, key logic) + 2. What JML clauses are needed? (requires, ensures, loop_invariant, assignable, decreases) + 3. What are the tricky parts? (loops, edge cases, array bounds, overflow) + + ## Plan + Write a concise step-by-step plan. High-level steps only, no tool calls. + + End with: + + Tools: + ``` + {%- for tool in tools.values() %} + - {{ tool.name }}: {{ tool.description }} + {%- endfor %} + ``` + + Task: + ``` + {{task}} + ``` + + update_plan_pre_messages: |- + You are refining your JML specification approach. + + Task: + ``` + {{task}} + ``` + + Review the verification history below and update your plan. + + update_plan_post_messages: |- + Based on verification results so far: + + ## What worked and what didn't + Key findings from previous attempts. + + ## Updated plan + Concise steps to complete the task. High-level only, no tool calls. + + End with: + + You have {{remaining_steps}} steps remaining. + + Tools: + ``` + {%- for tool in tools.values() %} + - {{ tool.name }}: {{ tool.description }} + {%- endfor %} + ``` + +task_complete: + pre_messages: |- + Summarize the final verified specification in one short paragraph. + post_messages: "" diff --git a/veriact/prompts/veriact_cli_prompt.yaml b/veriact/prompts/veriact_cli_prompt.yaml new file mode 100644 index 0000000..6b50a19 --- /dev/null +++ b/veriact/prompts/veriact_cli_prompt.yaml @@ -0,0 +1,156 @@ +system_prompt: |- + You are an expert Formal Verification Engineer. Given a Java program, synthesize JML specifications and iteratively verify them using OpenJML. + + You work in a thought -> tool -> observation loop. Each step you call ONE command-line tool and observe its JSON output. + + ## Output Format + + At each step, output exactly one JSON object — nothing else: + + {"thought": "your reasoning", "tool": "", "tool_input": { ... }} + + - "tool" must be one of: verify, run_spec_harness, task_complete. + - Provide the COMPLETE annotated Java source in tool_input each time you call verify or run_spec_harness. + - The class MUST be named Solution. + + ## Tools + + verify + tool_input: {"jml_annotated_code": ""} + Runs OpenJML ESC and returns the result WITH error analysis: + {"verified": bool, "return_code": int, "errors": [{"type","raw"}], + "failure_modes": [str], "repair_hints": [str], "summary": str, "raw_output": str} + Use at every verification attempt. Read repair_hints/summary to fix failures. + On Timeout (raw_output contains "Timeout"): STOP and simplify the spec before retrying. + NEVER resubmit the same or structurally identical spec after a timeout. + + run_spec_harness + tool_input: {"task_id": "", "jml_annotated_code": ""} + Evaluates JML quality on 4 metrics (all in [0.0, 1.0], 1.0 = perfect): + post_correctness - @ensures holds on all test inputs + post_completeness - @ensures is tight enough to kill output mutants + pre_correctness - @requires does not reject valid inputs + pre_completeness - @requires rejects invalid inputs + Returns: {task_id: {post_correctness, post_completeness, pre_correctness, pre_completeness}} + Call after verification passes. + + task_complete + tool_input: {"summary": ""} + Mark the task complete. Call as soon as the threshold below is met. + + ## Workflow + + 1. Analyze the Java method and infer its behavior. + 2. Synthesize JML (requires, ensures, loop_invariant, assignable, decreases as needed). + 3. Call verify. + - verified=false -> read repair_hints/summary, refine the spec, go to 3. + - Timeout -> simplify spec (see Timeout Strategy), go to 3. + - verified=true -> continue. + 4. Call run_spec_harness. + - If post_correctness < {{harness_threshold}} or post_completeness < {{harness_threshold}} -> refine spec, go to 3. + - If post_correctness >= {{harness_threshold}} and post_completeness >= {{harness_threshold}} -> call task_complete IMMEDIATELY. Do NOT refine further. + + ## Timeout Strategy + + Timeout means the SMT prover ran out of time. The spec is too complex, not necessarily wrong. + On timeout: do NOT resubmit the same spec; simplify (split compound invariants, remove nested + quantifiers, weaken temporarily, use \old sparingly, tighten assignable, prefer \result == expr + over \exists). On repeated timeouts, simplify further. Never revert to a timed-out spec. + + ## Spec Harness Score Enforcement + + After run_spec_harness, act IMMEDIATELY: + - post_correctness >= {{harness_threshold}} AND post_completeness >= {{harness_threshold}} -> call task_complete in your VERY NEXT step. Do NOT refine further. + - post_correctness < {{harness_threshold}} -> @ensures fails on some inputs; fix the postcondition. + - post_completeness < {{harness_threshold}} -> @ensures too weak; add more constraints. + + ## Example + + task_id = "maxElement_001" + + Step 1 - draft and verify: + {"thought": "maxElement returns the largest element. ensures result >= all elements and result is in the array.", "tool": "verify", "tool_input": {"jml_annotated_code": "public class Solution {\n /*@ requires arr != null && arr.length > 0;\n @ ensures (\\forall int i; 0 <= i && i < arr.length; arr[i] <= \\result);\n @ ensures (\\exists int i; 0 <= i && i < arr.length; arr[i] == \\result);\n @*/\n public static int maxElement(int[] arr) {\n int max = arr[0];\n for (int i = 1; i < arr.length; i++) { if (arr[i] > max) max = arr[i]; }\n return max;\n }\n}"}} + + Observation: {"verified": false, "failure_modes": ["PostconditionFailure"], "repair_hints": ["PostconditionFailure: ..."], "summary": "PostconditionFailure", "raw_output": "..."} + + Step 2 - add loop invariants and re-verify (tool=verify with the fixed code). + + Observation: {"verified": true, "return_code": 0, "errors": [], "summary": "No failures detected."} + + Step 3 - score: + {"thought": "Verification passed. Measuring spec quality.", "tool": "run_spec_harness", "tool_input": {"task_id": "maxElement_001", "jml_annotated_code": ""}} + + Observation: {"maxElement_001": {"post_correctness": 1.0, "post_completeness": 0.75, "pre_correctness": 1.0, "pre_completeness": 0.5}} + + Step 4 - threshold met, complete: + {"thought": "post_correctness=1.0 >= 0.5 and post_completeness=0.75 >= 0.5. Calling task_complete.", "tool": "task_complete", "tool_input": {"summary": "Verified JML for maxElement with loop invariants. post_correctness=1.0, post_completeness=0.75, pre_correctness=1.0, pre_completeness=0.5."}} + + Note: task_id is provided in the task description. + + Now Begin! + + Task: + ``` + {{task}} + ``` + +planning: + initial_plan: |- + Analyze the Java program and plan your JML specification approach. + + ## Analysis + 1. What does the method do? (inputs, outputs, key logic) + 2. What JML clauses are needed? (requires, ensures, loop_invariant, assignable, decreases) + 3. What are the tricky parts? (loops, edge cases, array bounds, overflow) + + ## Plan + Write a concise step-by-step plan. High-level steps only, no tool calls. + + End with: + + Tools: + ``` + {%- for tool in tools.values() %} + - {{ tool.name }}: {{ tool.description }} + {%- endfor %} + ``` + + Task: + ``` + {{task}} + ``` + + update_plan_pre_messages: |- + You are refining your JML specification approach. + + Task: + ``` + {{task}} + ``` + + Review the verification history below and update your plan. + + update_plan_post_messages: |- + Based on verification results so far: + + ## What worked and what didn't + Key findings from previous attempts. + + ## Updated plan + Concise steps to complete the task. High-level only, no tool calls. + + End with: + + You have {{remaining_steps}} steps remaining. + + Tools: + ``` + {%- for tool in tools.values() %} + - {{ tool.name }}: {{ tool.description }} + {%- endfor %} + ``` + +task_complete: + pre_messages: |- + Summarize the final verified specification and its spec-harness scores in one short paragraph. + post_messages: "" diff --git a/veriact/prompts/veriact_prompt.yaml b/veriact/prompts/veriact_prompt.yaml deleted file mode 100644 index 19bb412..0000000 --- a/veriact/prompts/veriact_prompt.yaml +++ /dev/null @@ -1,166 +0,0 @@ -system_prompt: |- - You are an expert Formal Verification Engineer. Given a Java program, synthesize JML specifications and iteratively verify them using OpenJML. - - You work in a thought -> code -> observation loop. - - ## Output Format - - At each step, output exactly one JSON object: - - {"thought": "your reasoning", "code": "python code to execute"} - - - Only output a JSON object. No text outside it. - - Code must be executable Python. Use print() to produce observations. - - Build annotated Java as a raw string: code = r'''...''' - - The class MUST be named Solution (file is always Solution.java). - - ## Tools - - verify_with_openjml(jml_annotated_code: str) -> str - Run OpenJML ESC on annotated Java code. - Returns: {"verified": bool, "return_code": int, "errors": [{"type": str, "raw": str}], "raw_output": str} - Use at every verification attempt. - On Timeout (raw_output contains "Timeout"): STOP. Simplify the spec before retrying. - NEVER resubmit the same or structurally identical spec after a timeout. - - analyze_openjml_errors(openjml_log: str) -> str - Classify OpenJML failures and provide targeted repair hints. - Returns: {"failure_modes": [str], "raw_errors": [str], "repair_hints": [str], "summary": str} - Call immediately after a failed verification. - - run_spec_harness(task_id: str, jml_annotated_code: str) -> str - Evaluate JML quality on 4 metrics (all in [0.0, 1.0], 1.0 = perfect): - post_correctness - @ensures holds on all test inputs - post_completeness - @ensures is tight enough to kill output mutants - pre_correctness - @requires does not reject valid inputs - pre_completeness - @requires rejects invalid inputs - Returns: {task_id: {post_correctness, post_completeness, pre_correctness, pre_completeness}} - Call after verification passes. - - task_complete(answer: str) -> str - Mark the task as complete. Call with a brief summary of the final specification and scores. - - ## Workflow - - 1. Analyze the Java method and infer its behavior. - 2. Synthesize JML (requires, ensures, loop_invariant, assignable, decreases as needed). - 3. Verify with verify_with_openjml. - - Failed -> call analyze_openjml_errors, refine spec, go to 3. - - Timeout -> simplify spec (see Timeout Strategy), go to 3. - - Passed -> continue. - 4. Evaluate with run_spec_harness. - - If post_correctness < {{harness_threshold}} or post_completeness < {{harness_threshold}} -> refine spec, go to 3. - - If post_correctness >= {{harness_threshold}} and post_completeness >= {{harness_threshold}} -> call task_complete IMMEDIATELY. Do NOT refine further. - - ## Timeout Strategy - - Timeout means the SMT prover ran out of time. The spec is too complex, not necessarily wrong. - - On timeout: - - Do NOT resubmit the same spec. - - Simplify: split compound invariants, remove nested quantifiers, weaken temporarily, - use \old sparingly, tighten assignable scope, prefer \result == expr over \exists. - - On repeated timeouts, simplify further. Never revert to a timed-out spec. - - ## Spec Harness Score Enforcement - - After calling run_spec_harness, check the scores and act IMMEDIATELY: - - - If post_correctness >= {{harness_threshold}} AND post_completeness >= {{harness_threshold}}: - -> STOP refinement. Call task_complete() in your VERY NEXT step. Do NOT refine further. - - If post_correctness < {{harness_threshold}}: @ensures fails on some inputs -> fix postcondition - - If post_completeness < {{harness_threshold}}: @ensures too weak -> add more constraints - - CRITICAL: Once both post_correctness and post_completeness meet the threshold (>= {{harness_threshold}}), you MUST call task_complete immediately. Do not attempt to improve scores further. - - ## Example - - task_id = "maxElement_001" - - Step 1 - Draft JML and verify: - {"thought": "maxElement returns the largest array element. Adding ensures: result >= all elements and result is in the array.", "code": "code = r'''\npublic class Solution {\n /*@ requires arr != null && arr.length > 0;\n @ ensures (\\forall int i; 0 <= i && i < arr.length; arr[i] <= \\result);\n @ ensures (\\exists int i; 0 <= i && i < arr.length; arr[i] == \\result);\n @*/\n public static int maxElement(int[] arr) {\n int max = arr[0];\n for (int i = 1; i < arr.length; i++) {\n if (arr[i] > max) max = arr[i];\n }\n return max;\n }\n}\n'''\nresult = verify_with_openjml(code)\nprint(result)"} - - Observation: {"verified": false, "errors": [{"type": "PostconditionFailure", "raw": "..."}], "raw_output": "..."} - - Step 2 - Analyze failure: - {"thought": "PostconditionFailure. Calling error analyzer for repair hints.", "code": "import json\nprev = json.loads(result)\nanalysis = analyze_openjml_errors(prev['raw_output'])\nprint(analysis)"} - - Observation: {"failure_modes": ["PostconditionFailure"], "repair_hints": ["Add loop invariants to help the prover establish the postcondition."], "summary": "PostconditionFailure"} - - Step 3 - Add loop invariants and re-verify: - {"thought": "Need loop invariants: i bounds, max >= all seen elements, max is one of them.", "code": "code = r'''\npublic class Solution {\n /*@ requires arr != null && arr.length > 0;\n @ ensures (\\forall int i; 0 <= i && i < arr.length; arr[i] <= \\result);\n @ ensures (\\exists int i; 0 <= i && i < arr.length; arr[i] == \\result);\n @*/\n public static int maxElement(int[] arr) {\n int max = arr[0];\n /*@ loop_invariant 1 <= i && i <= arr.length;\n @ loop_invariant (\\forall int k; 0 <= k && k < i; arr[k] <= max);\n @ loop_invariant (\\exists int k; 0 <= k && k < i; arr[k] == max);\n @ decreases arr.length - i;\n @*/\n for (int i = 1; i < arr.length; i++) {\n if (arr[i] > max) max = arr[i];\n }\n return max;\n }\n}\n'''\nresult = verify_with_openjml(code)\nprint(result)"} - - Observation: {"verified": true, "return_code": 0, "errors": [], "raw_output": ""} - - Step 4 - Evaluate spec quality: - {"thought": "Verification passed. Running harness to measure spec quality.", "code": "result = run_spec_harness('maxElement_001', code)\nprint(result)"} - - Observation: {"maxElement_001": {"post_correctness": 1.0, "post_completeness": 0.75, "pre_correctness": 1.0, "pre_completeness": 0.5}} - - Step 5 - Scores meet threshold, call task_complete: - {"thought": "post_correctness=1.0 >= 0.5 and post_completeness=0.75 >= 0.5. Both meet the threshold. Calling task_complete.", "code": "task_complete('Verified JML spec for maxElement with loop invariants. Scores: post_correctness=1.0, post_completeness=0.75, pre_correctness=1.0, pre_completeness=0.5.')"} - - Note: task_id is provided in the task description. - - Now Begin! - - Task: - ``` - {{task}} - ``` - -planning: - initial_plan: |- - Analyze the Java program and plan your JML specification approach. - - ## Analysis - 1. What does the method do? (inputs, outputs, key logic) - 2. What JML clauses are needed? (requires, ensures, loop_invariant, assignable, decreases) - 3. What are the tricky parts? (loops, edge cases, array bounds, overflow) - - ## Plan - Write a concise step-by-step plan. High-level steps only, no tool calls. - - End with: - - Tools: - ``` - {%- for tool in tools.values() %} - - {{ tool.name }}: {{ tool.description }} - {%- endfor %} - ``` - - Task: - ``` - {{task}} - ``` - - update_plan_pre_messages: |- - You are refining your JML specification approach. - - Task: - ``` - {{task}} - ``` - - Review the verification history below and update your plan. - - update_plan_post_messages: |- - Based on verification results so far: - - ## What worked and what didn't - Key findings from previous attempts. - - ## Updated plan - Concise steps to complete the task. High-level only, no tool calls. - - End with: - - You have {remaining_steps} steps remaining. - - Tools: - ``` - {%- for tool in tools.values() %} - - {{ tool.name }}: {{ tool.description }} - {%- endfor %} - ``` diff --git a/veriact/run/__init__.py b/veriact/run/__init__.py new file mode 100644 index 0000000..e69de29 diff --git a/veriact/run/run_batch.py b/veriact/run/run_batch.py index 9f25f0c..03616c8 100644 --- a/veriact/run/run_batch.py +++ b/veriact/run/run_batch.py @@ -28,8 +28,8 @@ VeriActAgent, VLLMModel, ) -from veriact.data_types import Task -from veriact.file_utility import dump_json, load_json, load_jsonl +from veriact.core.data_types import Task +from veriact.core.file_utility import dump_json, load_json, load_jsonl import veriact.config logger = logging.getLogger(__name__) @@ -86,6 +86,7 @@ def run_single_task( run_dir: str, max_steps: int, planning_interval: int, + no_harness: bool = False, ) -> dict: """Run a fresh VeriActAgent for a single task, sharing the same run directory.""" agent = VeriActAgent( @@ -94,6 +95,7 @@ def run_single_task( dataset_path=dataset_path, max_steps=max_steps, planning_interval=planning_interval, + no_harness=no_harness, _run_dir=run_dir, ) return agent.run(task) @@ -118,6 +120,7 @@ def main(): parser.add_argument("--openjml-path", default="openjml", help="Path to OpenJML binary (default: openjml)") parser.add_argument("--max-steps", type=int, default=15, help="Max agent steps per task (default: 15)") parser.add_argument("--planning_interval", type=int, default=5, help="Planning interval (default: 5)") + parser.add_argument("--no-harness", action="store_true", help="Ablation: run with verify + task_complete only (no run_spec_harness); success = verification passes") parser.add_argument("--task-ids", default=None, help="Path to a text file with one task_id per line to filter the benchmark") args = parser.parse_args() @@ -162,6 +165,7 @@ def main(): run_dir=run_dir, max_steps=args.max_steps, planning_interval=args.planning_interval, + no_harness=args.no_harness, ): task for task in tasks } diff --git a/veriact/run/run_single.py b/veriact/run/run_single.py index b07638f..d0148a0 100644 --- a/veriact/run/run_single.py +++ b/veriact/run/run_single.py @@ -23,8 +23,8 @@ VeriActAgent, VLLMModel, ) -from veriact.data_types import Task -from veriact.file_utility import dump_json, load_json, load_jsonl +from veriact.core.data_types import Task +from veriact.core.file_utility import dump_json, load_json, load_jsonl import veriact.config logger = logging.getLogger(__name__) @@ -79,6 +79,7 @@ def main(): parser.add_argument("--openjml-path", default="openjml", help="Path to OpenJML binary (default: openjml)") parser.add_argument("--max-steps", type=int, default=15, help="Max agent steps per task (default: 15)") parser.add_argument("--planning_interval", type=int, default=5, help="Planning interval (default: 5)") + parser.add_argument("--no-harness", action="store_true", help="Ablation: run with verify + task_complete only (no run_spec_harness); success = verification passes") args = parser.parse_args() logging.basicConfig(level=logging.INFO, format="%(asctime)s %(levelname)s %(name)s: %(message)s") @@ -107,6 +108,7 @@ def main(): output_dir=args.output_dir, max_steps=args.max_steps, planning_interval=args.planning_interval, + no_harness=args.no_harness, ) result = agent.run(task) completed.append(task.task_id) diff --git a/veriact/run/score_no_harness.py b/veriact/run/score_no_harness.py new file mode 100644 index 0000000..e731cff --- /dev/null +++ b/veriact/run/score_no_harness.py @@ -0,0 +1,140 @@ +#!/usr/bin/env python3 +"""Score a no-harness run's outputs with the spec-harness (offline). + +The ``--no-harness`` arm never calls ``run_spec_harness``, so its specs are left +unscored. This utility walks a run directory's per-task workspaces +(``/workspaces//``), runs the spec-harness on each task's final +``Solution.java`` (using the vendored ``harness/task.json`` for inputs/signature), +and writes a consolidated score table — so the no-harness arm can be compared to +the harness arm on identical metrics. + +Usage: + python -m veriact.run.score_no_harness \ + --run-dir out/veriact__gpt-4o__YYYYmmdd_HHMMSS \ + --openjml openjml --threads 4 +""" + +from __future__ import annotations + +import argparse +import csv +import json +import os +import sys +from concurrent.futures import ThreadPoolExecutor, as_completed + +from veriact.core.data_types import HARNESS_PASS_THRESHOLD +from veriact.tools.harness_tool import Task, evaluate_problem + +METRICS = ["post_correctness", "post_completeness", "pre_correctness", "pre_completeness"] + + +def _resolve_openjml(openjml: str) -> None: + """evaluate_problem invokes the literal binary 'openjml'; if a path is given, + prepend its dir to PATH so it resolves.""" + if openjml and openjml != "openjml" and os.sep in openjml: + d = os.path.dirname(os.path.abspath(openjml)) + os.environ["PATH"] = d + os.pathsep + os.environ.get("PATH", "") + + +def find_workspaces(run_dir: str) -> list[str]: + ws_root = os.path.join(run_dir, "workspaces") + if not os.path.isdir(ws_root): + return [] + out = [] + for name in sorted(os.listdir(ws_root)): + d = os.path.join(ws_root, name) + if os.path.isdir(d) and os.path.exists(os.path.join(d, "Solution.java")): + out.append(d) + return out + + +def score_workspace(ws: str, openjml: str, max_pairs: int, threshold: float) -> dict: + task_id = os.path.basename(ws) + row = {"task_id": task_id, **{m: None for m in METRICS}, "passed": False, "error": None} + sol = os.path.join(ws, "Solution.java") + tj = os.path.join(ws, "harness", "task.json") + if not os.path.exists(tj): + row["error"] = "missing harness/task.json" + return row + try: + code = open(sol).read() + task = Task.from_dict(json.load(open(tj))) + scores = evaluate_problem( + task, + llm_code=code, + openjml_path=openjml, + output_dir=os.path.join(ws, "harness"), + max_pairs=max_pairs, + run_id="score", + ) + except Exception as e: # noqa: BLE001 + row["error"] = str(e) + return row + if not scores: + row["error"] = "no test pairs could be parsed" + return row + row["task_id"] = scores.get("task_id", task_id) + for m in METRICS: + row[m] = scores.get(m, 0.0) + row["passed"] = ( + scores.get("post_correctness", 0.0) >= threshold + and scores.get("post_completeness", 0.0) >= threshold + ) + return row + + +def main(argv: list[str] | None = None) -> int: + p = argparse.ArgumentParser(description="Score a no-harness run with the spec-harness.") + p.add_argument("--run-dir", required=True, help="run dir containing workspaces/") + p.add_argument("--openjml", default=os.environ.get("OPENJML", "openjml")) + p.add_argument("--threads", type=int, default=4, help="parallel tasks (default: 4)") + p.add_argument("--max-pairs", type=int, default=5, dest="max_pairs") + p.add_argument("--threshold", type=float, default=HARNESS_PASS_THRESHOLD) + p.add_argument("--out", default=None, help="output prefix (default: /harness_scores)") + args = p.parse_args(argv) + + _resolve_openjml(args.openjml) + workspaces = find_workspaces(args.run_dir) + if not workspaces: + print(f"No workspaces with Solution.java under {args.run_dir}/workspaces", file=sys.stderr) + return 1 + + out_prefix = args.out or os.path.join(args.run_dir, "harness_scores") + print(f"Scoring {len(workspaces)} task(s) with spec-harness, threads={args.threads}") + + rows: list[dict] = [] + with ThreadPoolExecutor(max_workers=args.threads) as pool: + futs = { + pool.submit(score_workspace, ws, args.openjml, args.max_pairs, args.threshold): ws + for ws in workspaces + } + for fut in as_completed(futs): + row = fut.result() + rows.append(row) + tag = "err:" + row["error"] if row["error"] else f"pass={row['passed']}" + print(f" [{tag}] {row['task_id']}") + + rows.sort(key=lambda r: r["task_id"]) + fields = ["task_id", *METRICS, "passed", "error"] + with open(out_prefix + ".json", "w") as fh: + json.dump(rows, fh, indent=2) + with open(out_prefix + ".csv", "w", newline="") as fh: + w = csv.DictWriter(fh, fieldnames=fields) + w.writeheader() + w.writerows(rows) + + scored = [r for r in rows if r["error"] is None] + passed = sum(1 for r in scored if r["passed"]) + avg = { + m: round(sum(r[m] for r in scored if r[m] is not None) / len(scored), 3) + if scored else 0.0 + for m in METRICS + } + print(f"Scored {len(scored)}/{len(rows)} (passed={passed}); avg: {avg}") + print(f" -> {out_prefix}.json / {out_prefix}.csv") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/veriact/tool_validation.py b/veriact/tool_validation.py deleted file mode 100644 index 635fb60..0000000 --- a/veriact/tool_validation.py +++ /dev/null @@ -1,112 +0,0 @@ -"""AST-based validation for Tool classes.""" - -import ast -import builtins -from typing import Set - -from veriact.utility import BASE_BUILTIN_MODULES - -_BUILTIN_NAMES = set(vars(builtins)) - - -class MethodChecker(ast.NodeVisitor): - def __init__(self, class_attributes: Set[str], check_imports: bool = True): - self.undefined_names = set() - self.imports = {} - self.from_imports = {} - self.assigned_names = set() - self.arg_names = set() - self.class_attributes = class_attributes - self.errors = [] - self.check_imports = check_imports - self.typing_names = {"Any"} - - def visit_arguments(self, node): - self.arg_names = {arg.arg for arg in node.args} - if node.kwarg: self.arg_names.add(node.kwarg.arg) - if node.vararg: self.arg_names.add(node.vararg.arg) - - def visit_Import(self, node): - for name in node.names: - self.imports[name.asname or name.name] = name.name - - def visit_ImportFrom(self, node): - module = node.module or "" - for name in node.names: - self.from_imports[name.asname or name.name] = (module, name.name) - - def visit_Assign(self, node): - for target in node.targets: - if isinstance(target, ast.Name): - self.assigned_names.add(target.id) - self.visit(node.value) - - def visit_With(self, node): - for item in node.items: - if item.optional_vars and isinstance(item.optional_vars, ast.Name): - self.assigned_names.add(item.optional_vars.id) - self.generic_visit(node) - - def visit_ExceptHandler(self, node): - if node.name: - self.assigned_names.add(node.name) - self.generic_visit(node) - - def visit_AnnAssign(self, node): - if isinstance(node.target, ast.Name): - self.assigned_names.add(node.target.id) - if node.value: - self.visit(node.value) - - def visit_For(self, node): - target = node.target - if isinstance(target, ast.Name): - self.assigned_names.add(target.id) - elif isinstance(target, ast.Tuple): - for elt in target.elts: - if isinstance(elt, ast.Name): - self.assigned_names.add(elt.id) - self.generic_visit(node) - - def _handle_comprehension_generators(self, generators): - for gen in generators: - if isinstance(gen.target, ast.Name): - self.assigned_names.add(gen.target.id) - elif isinstance(gen.target, ast.Tuple): - for elt in gen.target.elts: - if isinstance(elt, ast.Name): - self.assigned_names.add(elt.id) - - def visit_ListComp(self, node): - self._handle_comprehension_generators(node.generators) - self.generic_visit(node) - def visit_DictComp(self, node): - self._handle_comprehension_generators(node.generators) - self.generic_visit(node) - def visit_SetComp(self, node): - self._handle_comprehension_generators(node.generators) - self.generic_visit(node) - - def visit_Attribute(self, node): - if not (isinstance(node.value, ast.Name) and node.value.id == "self"): - self.generic_visit(node) - - def _is_defined(self, name): - return ( - name in _BUILTIN_NAMES or name in BASE_BUILTIN_MODULES - or name in self.arg_names or name == "self" - or name in self.class_attributes or name in self.imports - or name in self.from_imports or name in self.assigned_names - or name in self.typing_names - ) - - def visit_Name(self, node): - if isinstance(node.ctx, ast.Load) and not self._is_defined(node.id): - self.errors.append(f"Name '{node.id}' is undefined.") - - def visit_Call(self, node): - if isinstance(node.func, ast.Name) and not self._is_defined(node.func.id): - self.errors.append(f"Name '{node.func.id}' is undefined.") - self.generic_visit(node) - - diff --git a/veriact/tools.py b/veriact/tools.py deleted file mode 100644 index 19a4d9a..0000000 --- a/veriact/tools.py +++ /dev/null @@ -1,232 +0,0 @@ -"""VeriAct tool suite — Tool subclasses with stubs for forward().""" - -import json -import logging -import os - -from veriact.harness_tool import Task, evaluate_problem -from veriact.tools_base import Tool -from veriact.verifier_tool import ( - VerificationResult, - classify_failures, - extract_errors, - verify_with_openjml as _verify_with_openjml, -) - -logger = logging.getLogger(__name__) - - -REPAIR_HINTS: dict[str, str] = { - "SyntaxError": "Fix JML syntax (missing semicolons, wrong keywords).", - "PostconditionFailure": "The @ensures clause is logically incorrect.", - "ExceptionalPostconditionFailure": "The @signals clause is incorrect.", - "PreconditionFailure": "The @requires clause is too weak or wrong.", - "LoopInvariantFailure": "The @maintaining clause doesn't hold.", - "RankingFunctionFailure": "The @decreases expression is wrong.", - "AssignableFailure": "The @assignable clause is too permissive or missing.", - "ArrayIndex": "Missing array bounds check in @requires.", - "NegativeSize": "Array size may be negative; add check in @requires.", - "NullDeReference": "Missing null check in @requires.", - "NullUnbox": "Potential null unboxing; add null check in @requires.", - "DivideByZero": "Missing division-by-zero guard in @requires.", - "ArithmeticOperationRange": "Integer overflow not guarded in @requires.", - "ArithmeticCastRange": "Cast may overflow; add range guard in @requires.", - "BadCast": "Unsafe cast; add type guard in @requires.", - "BadArrayAssignment": "Incompatible array assignment; check element types.", - "CalledMethodPrecondition": "Called method precondition not met; strengthen @requires.", - "LargeShift": "Shift amount out of range; add bounds check in @requires.", - "AssertFailure": "An @assert statement fails; check the invariant.", - "UnknownVerificationFailure": "Unknown verification failure; review the full OpenJML log.", -} - - -class VerifyJMLTool(Tool): - """Verify JML-annotated Java code using OpenJML (ESC mode).""" - - name = "verify_with_openjml" - description = ( - "Run OpenJML Extended Static Checking on JML-annotated Java code. " - "Returns verification status (verified/failed/unknown) and any error " - "messages from the verifier. Error messages include line numbers and " - "specific failure reasons." - ) - inputs = { - "jml_annotated_code": { - "type": "string", - "description": "Complete Java source with JML annotations.", - } - } - output_type = "string" - - def __init__(self, openjml_path: str = "openjml", output_dir: str = "veriact_outputs"): - super().__init__() - self._openjml_path = openjml_path - self._output_dir = os.path.join(output_dir, "tmp") - - def forward(self, jml_annotated_code: str) -> str: - result: VerificationResult = _verify_with_openjml( - jml_annotated_code, - classname="Solution", - output_dir=self._output_dir, - ) - return json.dumps( - { - "verified": result.success, - "return_code": result.return_code, - "errors": result.classified_errors, - "raw_output": result.error_log, - } - ) - - -class AnalyzeErrorTool(Tool): - """Classify failure modes from OpenJML output.""" - - name = "analyze_openjml_errors" - description = ( - "Analyze verification results to classify failures and produce repair hints." - ) - inputs = { - "openjml_log": {"type": "string", "description": "Raw OpenJML output."}, - } - output_type = "string" - - def forward(self, openjml_log: str) -> str: - errors = extract_errors(openjml_log) - - failure_modes: list[str] = [] - raw_errors: list[str] = [] - repair_hints: list[str] = [] - seen_hints: set[str] = set() - - for error_level, error_msg in errors: - failure_type = classify_failures(error_level, error_msg) - failure_modes.append(failure_type) - raw_errors.append(error_msg[:500]) - hint = REPAIR_HINTS.get(failure_type) - if hint and failure_type not in seen_hints: - repair_hints.append(f"{failure_type}: {hint}") - seen_hints.add(failure_type) - - if failure_modes: - counts: dict[str, int] = {} - for fm in failure_modes: - counts[fm] = counts.get(fm, 0) + 1 - summary = ", ".join( - f"{t} (x{c})" if c > 1 else t for t, c in counts.items() - ) - else: - summary = "No failures detected." - - return json.dumps( - { - "failure_modes": failure_modes, - "raw_errors": raw_errors, - "repair_hints": repair_hints, - "summary": summary, - } - ) - - -class RunHarnessTool(Tool): - """Evaluate spec quality using the spec-harness 4-metric.""" - - name = "run_spec_harness" - description = ( - "Evaluate JML spec quality: PostCorrectness, PostCompleteness, " - "PreCorrectness, PreCompleteness. Returns scores for each metric." - ) - inputs = { - "task_id": { - "type": "string", - "description": "Identifier for the task being evaluated.", - }, - "jml_annotated_code": { - "type": "string", - "description": "LLM generated complete Java source with JML annotations.", - }, - } - output_type = "string" - - def __init__(self, openjml_path: str = "openjml", dataset_path: str = "", output_dir: str = "veriact_outputs"): - super().__init__() - self._openjml_path = openjml_path - self._dataset_path = dataset_path - self._output_dir = output_dir - self._task_cache: dict[str, Task] = {} - self._run_counter: dict[str, int] = {} # per-task run counter - - def _load_task(self, task_id: str) -> Task: - if task_id in self._task_cache: - return self._task_cache[task_id] - if not self._dataset_path: - raise ValueError( - "dataset_path not configured; cannot look up task by id. " - "Pass dataset_path= when constructing RunHarnessTool." - ) - with open(self._dataset_path) as fh: - raw = fh.read().strip() - if raw.startswith("["): - records = json.loads(raw) - else: - records = [json.loads(line) for line in raw.splitlines() if line.strip()] - for data in records: - if data.get("task_id") == task_id: - task = Task.from_dict(data) - self._task_cache[task_id] = task - return task - raise KeyError( - f"task_id '{task_id}' not found in dataset '{self._dataset_path}'" - ) - - def forward(self, task_id: str, jml_annotated_code: str) -> str: - try: - task = self._load_task(task_id) - except (ValueError, KeyError, FileNotFoundError) as exc: - return json.dumps({"error": str(exc), "task_id": task_id}) - - # Increment run counter for this task - self._run_counter[task_id] = self._run_counter.get(task_id, 0) + 1 - run_id = f"run_{self._run_counter[task_id]}" - - scores = evaluate_problem( - task, - llm_code=jml_annotated_code, - openjml_path=self._openjml_path, - output_dir=self._output_dir, - run_id=run_id, - ) - - if not scores: - return json.dumps( - { - "error": "No test pairs could be parsed for this task.", - "task_id": task_id, - } - ) - - return json.dumps( - { - task_id: { - "post_correctness": scores.get("post_correctness", 0.0), - "post_completeness": scores.get("post_completeness", 0.0), - "pre_correctness": scores.get("pre_correctness", 0.0), - "pre_completeness": scores.get("pre_completeness", 0.0), - } - } - ) - - -def get_veriact_tools( - openjml_path: str = "openjml", - dataset_path: str = "", - output_dir: str = "veriact_outputs", -) -> list[Tool]: - return [ - VerifyJMLTool(openjml_path=openjml_path, output_dir=output_dir), - AnalyzeErrorTool(), - RunHarnessTool(openjml_path=openjml_path, dataset_path=dataset_path, output_dir=output_dir), - ] - - -TOOL_NAMES = ["verify_with_openjml", "analyze_openjml_errors", "run_spec_harness"] diff --git a/veriact/tools/__init__.py b/veriact/tools/__init__.py new file mode 100644 index 0000000..e69de29 diff --git a/veriact/tools/base.py b/veriact/tools/base.py index 8ffe1d1..f91fc14 100644 --- a/veriact/tools/base.py +++ b/veriact/tools/base.py @@ -1,19 +1,17 @@ -"""Tool base class and utilities for agent tool definitions.""" +"""Tool base class for agent tool definitions (trimmed for veriact). + +Only what veriact needs: attribute/signature validation and a callable +interface. The original ``to_dict``/``save``/``from_code`` serialization helpers +(which pulled in extra type-hint/AST utilities) are omitted. +""" -import ast import inspect -import json import logging -import sys -import types from functools import wraps -from pathlib import Path from typing import Dict, Union -from veriact._function_type_hints_utils import get_imports -from veriact.agent_types import handle_agent_input_types, handle_agent_output_types -from veriact.tool_validation import MethodChecker -from veriact.utility import get_source, instance_to_source, is_valid_name +from veriact.core.agent_types import handle_agent_input_types, handle_agent_output_types +from veriact.core.utility import is_valid_name logger = logging.getLogger(__name__) @@ -23,10 +21,12 @@ def validate_after_init(cls): original_init = cls.__init__ + @wraps(original_init) def new_init(self, *args, **kwargs): original_init(self, *args, **kwargs) self.validate_arguments() + cls.__init__ = new_init return cls @@ -88,33 +88,3 @@ def __call__(self, *args, sanitize_inputs_outputs: bool = False, **kwargs): def setup(self): self.is_initialized = True - - def to_dict(self) -> dict: - cls_name = self.__class__.__name__ - if cls_name == "SimpleTool": - source_code = get_source(self.forward).replace("@tool", "") - mc = MethodChecker(set()) - mc.visit(ast.parse(source_code)) - tool_code = "from typing import Any, Optional\n" + source_code - else: - tool_code = "from typing import Any, Optional\n" + instance_to_source(self, base_cls=Tool) - requirements = {el for el in get_imports(tool_code) if el not in sys.stdlib_module_names} - return {"name": self.name, "code": tool_code, "requirements": sorted(requirements)} - - def save(self, output_dir: str | Path, tool_file_name: str = "tool", make_gradio_app: bool = True): - output_path = Path(output_dir) - output_path.mkdir(parents=True, exist_ok=True) - (output_path / f"{tool_file_name}.py").write_text(self.to_dict()["code"], encoding="utf-8") - - @classmethod - def from_code(cls, tool_code: str, **kwargs): - module = types.ModuleType("dynamic_tool") - exec(tool_code, module.__dict__) - tool_class = next((obj for _, obj in inspect.getmembers(module, inspect.isclass) if issubclass(obj, Tool) and obj is not Tool), None) - if tool_class is None: - raise ValueError("No Tool subclass found.") - if not isinstance(tool_class.inputs, dict): - tool_class.inputs = ast.literal_eval(tool_class.inputs) - return tool_class(**kwargs) - - diff --git a/veriact/tools/cli.py b/veriact/tools/cli.py new file mode 100644 index 0000000..ef1afe5 --- /dev/null +++ b/veriact/tools/cli.py @@ -0,0 +1,196 @@ +#!/usr/bin/env python3 +"""veriact tool CLI — the three agent tools as subcommands. + +The CLI-ReAct agent ([cli_agent.py]) drives these as subprocesses and observes +their JSON stdout: + + verify run OpenJML ESC on the given code; output includes the error + analysis (failure modes + repair hints) — analyze is merged in + harness score the spec on the four spec-harness metrics + submit record the final submission (task_complete) + +No attempt budget here: the agent's loop is bounded by --max-steps instead. +""" + +from __future__ import annotations + +import argparse +import json +import os +import sys + +# Import the scorer/verifier whether run as `-m veriact.tools.cli` or by file path. +try: + from veriact.tools.harness_tool import Task, evaluate_problem + from veriact.tools.verifier_tool import VerificationResult, verify_with_openjml +except ImportError: # invoked directly by path (the agent does this) + sys.path.insert(0, os.path.dirname(os.path.abspath(__file__))) + from harness_tool import Task, evaluate_problem # type: ignore + from verifier_tool import VerificationResult, verify_with_openjml # type: ignore + +# Repair hints — same mapping VeriAct's analyze tool uses. +REPAIR_HINTS: dict[str, str] = { + "SyntaxError": "Fix JML syntax (missing semicolons, wrong keywords).", + "PostconditionFailure": "The @ensures clause is logically incorrect.", + "ExceptionalPostconditionFailure": "The @signals clause is incorrect.", + "PreconditionFailure": "The @requires clause is too weak or wrong.", + "LoopInvariantFailure": "The @maintaining clause doesn't hold.", + "RankingFunctionFailure": "The @decreases expression is wrong.", + "AssignableFailure": "The @assignable clause is too permissive or missing.", + "ArrayIndex": "Missing array bounds check in @requires.", + "NegativeSize": "Array size may be negative; add check in @requires.", + "NullDeReference": "Missing null check in @requires.", + "NullUnbox": "Potential null unboxing; add null check in @requires.", + "DivideByZero": "Missing division-by-zero guard in @requires.", + "ArithmeticOperationRange": "Integer overflow not guarded in @requires.", + "ArithmeticCastRange": "Cast may overflow; add range guard in @requires.", + "BadCast": "Unsafe cast; add type guard in @requires.", + "BadArrayAssignment": "Incompatible array assignment; check element types.", + "CalledMethodPrecondition": "Called method precondition not met; strengthen @requires.", + "LargeShift": "Shift amount out of range; add bounds check in @requires.", + "AssertFailure": "An @assert statement fails; check the invariant.", + "UnknownVerificationFailure": "Unknown verification failure; review the full OpenJML log.", +} + + +def _resolve_openjml(openjml: str) -> None: + """verify_with_openjml/evaluate_problem invoke the literal binary 'openjml'; + if a path is given, prepend its dir to PATH so that resolves to it.""" + if openjml and openjml != "openjml" and os.sep in openjml: + d = os.path.dirname(os.path.abspath(openjml)) + os.environ["PATH"] = d + os.pathsep + os.environ.get("PATH", "") + + +def _default_openjml(arg: str | None) -> str: + return arg or os.environ.get("OPENJML", "openjml") + + +def _read(path: str) -> str: + with open(path) as fh: + return fh.read() + + +def _emit(obj) -> None: + print(json.dumps(obj, indent=2)) + + +def _analyze(classified_errors: list[dict]) -> dict: + failure_modes, repair_hints, seen = [], [], set() + for err in classified_errors: + ftype = err.get("type", "UnknownVerificationFailure") + failure_modes.append(ftype) + hint = REPAIR_HINTS.get(ftype) + if hint and ftype not in seen: + repair_hints.append(f"{ftype}: {hint}") + seen.add(ftype) + if failure_modes: + counts: dict[str, int] = {} + for fm in failure_modes: + counts[fm] = counts.get(fm, 0) + 1 + summary = ", ".join(f"{t} (x{c})" if c > 1 else t for t, c in counts.items()) + else: + summary = "No failures detected." + return {"failure_modes": failure_modes, "repair_hints": repair_hints, "summary": summary} + + +def cmd_verify(args: argparse.Namespace) -> int: + _resolve_openjml(_default_openjml(args.openjml)) + code = _read(args.code) + result: VerificationResult = verify_with_openjml( + code, classname="Solution", output_dir=args.output_dir or "veriact_tmp" + ) + analysis = _analyze(result.classified_errors) + _emit( + { + "verified": result.success, + "return_code": result.return_code, + "errors": result.classified_errors, + "failure_modes": analysis["failure_modes"], + "repair_hints": analysis["repair_hints"], + "summary": analysis["summary"], + "raw_output": result.error_log, + } + ) + return 0 + + +def cmd_harness(args: argparse.Namespace) -> int: + openjml = _default_openjml(args.openjml) + _resolve_openjml(openjml) + code = _read(args.code) + with open(args.task_json) as fh: + task = Task.from_dict(json.load(fh)) + scores = evaluate_problem( + task, + llm_code=code, + openjml_path=openjml, + output_dir=args.output_dir or "veriact_tmp", + max_pairs=args.max_pairs, + run_id=args.run_id or "", + ) + if not scores: + _emit({"error": "No test pairs could be parsed.", "task_id": task.task_id}) + return 1 + _emit( + { + task.task_id: { + "post_correctness": scores.get("post_correctness", 0.0), + "post_completeness": scores.get("post_completeness", 0.0), + "pre_correctness": scores.get("pre_correctness", 0.0), + "pre_completeness": scores.get("pre_completeness", 0.0), + } + } + ) + return 0 + + +def cmd_submit(args: argparse.Namespace) -> int: + import datetime + + code = _read(args.code) if args.code and os.path.exists(args.code) else "" + submission = { + "summary": args.summary, + "final_code": code, + "timestamp": datetime.datetime.now().isoformat(timespec="seconds"), + } + if args.out: + with open(args.out, "w") as fh: + json.dump(submission, fh, indent=2) + _emit({"submitted": True, "summary": args.summary, "path": args.out}) + return 0 + + +def build_parser() -> argparse.ArgumentParser: + p = argparse.ArgumentParser(prog="veriact.tools.cli") + sub = p.add_subparsers(dest="command", required=True) + + pv = sub.add_parser("verify", help="OpenJML ESC + error analysis") + pv.add_argument("--code", required=True) + pv.add_argument("--openjml") + pv.add_argument("--output-dir", dest="output_dir") + pv.set_defaults(func=cmd_verify) + + ph = sub.add_parser("harness", help="spec-harness 4-metric scoring") + ph.add_argument("--code", required=True) + ph.add_argument("--task-json", dest="task_json", required=True) + ph.add_argument("--openjml") + ph.add_argument("--output-dir", dest="output_dir") + ph.add_argument("--max-pairs", type=int, default=5, dest="max_pairs") + ph.add_argument("--run-id", dest="run_id") + ph.set_defaults(func=cmd_harness) + + ps = sub.add_parser("submit", help="record the final submission") + ps.add_argument("summary") + ps.add_argument("--code") + ps.add_argument("--out") + ps.set_defaults(func=cmd_submit) + return p + + +def main(argv: list[str] | None = None) -> int: + args = build_parser().parse_args(argv) + return args.func(args) + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/veriact/tools/default_tools.py b/veriact/tools/default_tools.py index cb59e7d..3f6f3f1 100644 --- a/veriact/tools/default_tools.py +++ b/veriact/tools/default_tools.py @@ -1,6 +1,6 @@ """Default agent tools (TaskCompletionTool).""" -from veriact.tools_base import Tool +from veriact.tools.base import Tool class TaskCompletionTool(Tool): diff --git a/veriact/tools/descriptors.py b/veriact/tools/descriptors.py new file mode 100644 index 0000000..9c59572 --- /dev/null +++ b/veriact/tools/descriptors.py @@ -0,0 +1,52 @@ +"""Tool *descriptors* for the CLI-ReAct agent. + +These exist for prompt rendering, planning, and trajectory metadata (name / +description / inputs). They are **not** executed via ``forward`` — the CLIAgent +dispatches each tool name to a CLI subprocess (see [cli_agent.py]) and observes +its stdout. ``forward`` is therefore a stub kept only to satisfy the Tool base. +""" + +from veriact.tools.base import Tool + + +class VerifyTool(Tool): + name = "verify" + description = ( + "Run OpenJML Extended Static Checking on the given JML-annotated Java " + "code. Returns verification status plus error analysis (failure modes " + "and repair hints): {verified, return_code, errors, failure_modes, " + "repair_hints, summary, raw_output}." + ) + inputs = { + "jml_annotated_code": { + "type": "string", + "description": "Complete Java source (class Solution) with JML annotations.", + } + } + output_type = "string" + + def forward(self, jml_annotated_code: str) -> str: # pragma: no cover - dispatched via CLI + raise NotImplementedError("verify is executed as a CLI subprocess by CLIAgent") + + +class RunHarnessTool(Tool): + name = "run_spec_harness" + description = ( + "Evaluate JML spec quality on four metrics in [0,1]: post_correctness, " + "post_completeness, pre_correctness, pre_completeness. Call after " + "verification passes." + ) + inputs = { + "task_id": { + "type": "string", + "description": "Identifier of the task being evaluated.", + }, + "jml_annotated_code": { + "type": "string", + "description": "Complete Java source (class Solution) with JML annotations.", + }, + } + output_type = "string" + + def forward(self, task_id: str, jml_annotated_code: str) -> str: # pragma: no cover + raise NotImplementedError("run_spec_harness is executed as a CLI subprocess by CLIAgent")