From 93d4c4ded4446b8a70faca46efeb6a2c53d68227 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Sun, 28 Jun 2026 22:15:15 +0300 Subject: [PATCH 1/6] fix case of no udts crashing the pipeline --- composer/spec/source/summarizer.py | 18 ++++++++++++++---- tests/test_summarizer.py | 24 ++++++++++++++++++++++++ 2 files changed, 38 insertions(+), 4 deletions(-) create mode 100644 tests/test_summarizer.py diff --git a/composer/spec/source/summarizer.py b/composer/spec/source/summarizer.py index 75e7628..200b83b 100644 --- a/composer/spec/source/summarizer.py +++ b/composer/spec/source/summarizer.py @@ -76,6 +76,19 @@ def _format_types(udts: list[dict]) -> str: return "\n".join(to_format) +def _types_input(udts: str) -> list[str | dict]: + """Initial-prompt fragment advertising the available user-defined types. + + Returns [] when there are none — never a list containing an empty string, + which would become an empty Anthropic text content block and get the whole + request rejected ("messages: text content blocks must be non-empty"). The + return type mirrors ``FlowInput.input`` so it drops straight into ``Input``. + """ + if not udts: + return [] + return ["The following types are available for use in your spec", udts] + + class SummarizerExtra(TypedDict): plan: str | None curr_spec: str | None @@ -251,10 +264,7 @@ def _validator(s: ST, _res: str) -> str | None: typechecked="", plan=None, curr_spec=None, - input=[ - "The following types are available for use in your spec", - udts, - ], + input=_types_input(udts), ), thread_id=ctx.thread_id, recursion_limit=ctx.recursion_limit, diff --git a/tests/test_summarizer.py b/tests/test_summarizer.py new file mode 100644 index 0000000..2032aee --- /dev/null +++ b/tests/test_summarizer.py @@ -0,0 +1,24 @@ +"""Unit tests for composer.spec.source.summarizer input construction. + +Regression guard: a contract with no user-defined types must not cause an empty +text content block to be sent to the LLM (Anthropic rejects those with +"messages: text content blocks must be non-empty"). +""" + +from composer.spec.source.summarizer import _format_types, _types_input + + +def test_format_types_empty(): + assert _format_types([]) == "" + + +def test_types_input_empty_is_omitted(): + # The bug: an empty udts must yield no input element, never [""]. + assert _types_input("") == [] + + +def test_types_input_nonempty_keeps_preamble(): + assert _types_input("A struct Foo at the top level: use `Foo`") == [ + "The following types are available for use in your spec", + "A struct Foo at the top level: use `Foo`", + ] From fe8d7c2716137df66cd1964b38c04fd72699c6bb Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Mon, 29 Jun 2026 01:48:42 +0300 Subject: [PATCH 2/6] fix autosetup that on second call invokes astextraction, but does not deal with Warnings and Errors prepended before the actual json in stdout. We drop the non-json messages and handle with proper logging any remaining json decode errors --- certora_autosetup/setup/summary_resolver.py | 40 +++++++++++++---- tests/test_summary_resolver.py | 48 +++++++++++++++++++++ 2 files changed, 79 insertions(+), 9 deletions(-) create mode 100644 tests/test_summary_resolver.py diff --git a/certora_autosetup/setup/summary_resolver.py b/certora_autosetup/setup/summary_resolver.py index 6cbec9d..56dd2c6 100644 --- a/certora_autosetup/setup/summary_resolver.py +++ b/certora_autosetup/setup/summary_resolver.py @@ -105,6 +105,36 @@ def _vmtype_to_str(vmtype: dict) -> str: return base +def _parse_ast_payload(stdout: str, returncode: int, stderr: str) -> Optional[dict]: + """Parse the JSON AST payload from ``ASTExtraction.jar`` stdout. + + The jar prints ``Warning: …`` / ``Error: …`` + diagnostic lines to stdout *before* the JSON payload, which it then prints + exactly once as the final output (on both the success and syntax-error paths). + So we drop the leading diagnostic lines and parse the remainder — rather than + ``json.loads`` the whole stream, which fails at char 0 on the first warning. + Returns the decoded payload, or ``None`` when the jar produced no AST + (``ast`` is null — a hard syntax error left for the TypecheckerLoop backstop). + """ + lines = stdout.splitlines() + # Only LEADING diagnostic lines precede the JSON; never strip inside the payload. + while lines and (lines[0].startswith("Warning: ") or lines[0].startswith("Error: ")): + lines.pop(0) + body = "\n".join(lines).strip() + # Empty stdout (or stdout that was nothing but diagnostics) means the jar gave us + # no payload — surface that with its stderr rather than an opaque JSONDecodeError. + if not body: + raise RuntimeError(f"{_AST_EXTRACTION_JAR} produced no JSON (exit {returncode}): {stderr.strip()}") + try: + payload = json.loads(body) + except json.JSONDecodeError as exc: + raise RuntimeError( + f"{_AST_EXTRACTION_JAR} output was not JSON after stripping diagnostics " + f"(exit {returncode}): {exc}; stdout_head={stdout[:300]!r} stderr={stderr.strip()[:500]!r}" + ) + return payload if payload.get("ast") else None + + def _ast_extraction(blanked_source: str) -> Optional[dict]: """Run ``ASTExtraction.jar syntax-check`` on CVL source, return the parsed JSON. @@ -125,15 +155,7 @@ def _ast_extraction(blanked_source: str) -> Optional[dict]: capture_output=True, text=True, ) - # The jar prints the JSON payload to stdout even for syntax errors (ast=null). Empty - # stdout means it crashed before producing anything — surface that, with its stderr, - # rather than an opaque JSONDecodeError. - if not result.stdout.strip(): - raise RuntimeError( - f"{_AST_EXTRACTION_JAR} produced no output (exit {result.returncode}): {result.stderr.strip()}" - ) - payload = json.loads(result.stdout) - return payload if payload.get("ast") else None + return _parse_ast_payload(result.stdout, result.returncode, result.stderr) def parse_methods_entries(spec_path: Path, log: Optional[LogFn] = None) -> List[MethodEntry]: diff --git a/tests/test_summary_resolver.py b/tests/test_summary_resolver.py new file mode 100644 index 0000000..510c9b2 --- /dev/null +++ b/tests/test_summary_resolver.py @@ -0,0 +1,48 @@ +"""Unit tests for ASTExtraction stdout parsing in summary_resolver. + +Regression guard: ASTExtraction.jar (EVMVerifier OutPrinter) prints `Warning:` +diagnostic lines to stdout before the JSON payload, so a raw json.loads of stdout +fails at char 0. `_parse_ast_payload` must strip those leading lines and parse the +JSON that follows. +""" + +import json + +import pytest + +from certora_autosetup.setup.summary_resolver import _parse_ast_payload + +_AST = {"ast": {"importedMethods": []}} +_AST_JSON = json.dumps(_AST) + + +def test_pure_json_no_warnings(): + assert _parse_ast_payload(_AST_JSON, 0, "") == _AST + + +def test_warning_lines_before_json_are_stripped(): + stdout = ( + "Warning: Syntax warning in spec file dummy file:1:1: Registered the contract alias x\n" + "Warning: Syntax warning in spec file dummy file:2:1: Registered the contract alias y\n" + + _AST_JSON + ) + assert _parse_ast_payload(stdout, 0, "") == _AST + + +def test_ast_null_returns_none(): + assert _parse_ast_payload(json.dumps({"ast": None}), 1, "") is None + + +def test_empty_stdout_raises_with_exit_and_stderr(): + with pytest.raises(RuntimeError, match="produced no JSON.*exit 3.*boom"): + _parse_ast_payload("", 3, "boom") + + +def test_warnings_only_no_json_raises(): + with pytest.raises(RuntimeError, match="produced no JSON"): + _parse_ast_payload("Warning: something\n", 0, "") + + +def test_non_json_after_stripping_raises_with_context(): + with pytest.raises(RuntimeError, match="was not JSON after stripping diagnostics"): + _parse_ast_payload("Warning: w\nnot json at all", 0, "stderr text") From 17953ef2b07313d4d59d87cac33b8a21bdda93aa Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Mon, 29 Jun 2026 02:00:21 +0300 Subject: [PATCH 3/6] Make summary_resolver importable without certora_cli (lazy find_jar) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The pure _parse_ast_payload parser is unit-tested in the cheap pytest CI job, which installs deps without the prover extra (no certora_cli). The module-level `from certora_cli... import find_jar` made importing the module — and thus collecting tests/test_summary_resolver.py — fail with ModuleNotFoundError. find_jar is the only certora_cli symbol in this module's import chain, so defer it into _ast_extraction (matching existing lazy-import patterns in the package). The module now imports without certora_cli; the parser test runs in fast CI. Co-Authored-By: Claude Opus 4.8 (1M context) --- certora_autosetup/setup/summary_resolver.py | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/certora_autosetup/setup/summary_resolver.py b/certora_autosetup/setup/summary_resolver.py index 56dd2c6..18b55b9 100644 --- a/certora_autosetup/setup/summary_resolver.py +++ b/certora_autosetup/setup/summary_resolver.py @@ -38,8 +38,6 @@ from pathlib import Path from typing import Callable, Dict, List, Optional, Sequence, Set, Tuple -from certora_cli.Shared.certoraUtils import find_jar - from certora_autosetup.parsers.method_parser import MethodParser # A logger callable matching SummarySetup.log(message, level). @@ -144,6 +142,10 @@ def _ast_extraction(blanked_source: str) -> Optional[dict]: Non-fatal diagnostics (e.g. "no reason provided for assumption") still yield an AST and are ignored here. """ + # find_jar is the only certora_cli dependency in this module; import it lazily so + # summary_resolver stays importable (e.g. for unit tests) without the prover CLI. + from certora_cli.Shared.certoraUtils import find_jar + # find_jar only computes a path; it does not verify the jar is present. Fail loud # here rather than letting `java -jar ` die with an opaque JSONDecodeError. jar = find_jar(_AST_EXTRACTION_JAR) From b99a03062fc6c90b09d928228298853074e82ba8 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Mon, 29 Jun 2026 02:03:19 +0300 Subject: [PATCH 4/6] Install prover extra in pytest CI instead of deferring find_jar import The cheap pytest job synced deps without certora_cli, so collecting tests/test_summary_resolver.py (which imports certora_autosetup.setup. summary_resolver -> certora_cli find_jar) failed with ModuleNotFoundError. Provide the dependency in CI (`uv sync --group test --extra prover`) rather than contorting the module to import without it. Reverts the lazy-import change from 17953ef; summary_resolver keeps its top-level find_jar import. Co-Authored-By: Claude Opus 4.8 (1M context) --- .github/workflows/pytest.yml | 2 +- certora_autosetup/setup/summary_resolver.py | 6 ++---- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/.github/workflows/pytest.yml b/.github/workflows/pytest.yml index 432c1c2..184f7c2 100644 --- a/.github/workflows/pytest.yml +++ b/.github/workflows/pytest.yml @@ -23,7 +23,7 @@ jobs: - name: sync-deps run: | - uv sync --group test + uv sync --group test --extra prover - name: Run pytest run: | diff --git a/certora_autosetup/setup/summary_resolver.py b/certora_autosetup/setup/summary_resolver.py index 18b55b9..56dd2c6 100644 --- a/certora_autosetup/setup/summary_resolver.py +++ b/certora_autosetup/setup/summary_resolver.py @@ -38,6 +38,8 @@ from pathlib import Path from typing import Callable, Dict, List, Optional, Sequence, Set, Tuple +from certora_cli.Shared.certoraUtils import find_jar + from certora_autosetup.parsers.method_parser import MethodParser # A logger callable matching SummarySetup.log(message, level). @@ -142,10 +144,6 @@ def _ast_extraction(blanked_source: str) -> Optional[dict]: Non-fatal diagnostics (e.g. "no reason provided for assumption") still yield an AST and are ignored here. """ - # find_jar is the only certora_cli dependency in this module; import it lazily so - # summary_resolver stays importable (e.g. for unit tests) without the prover CLI. - from certora_cli.Shared.certoraUtils import find_jar - # find_jar only computes a path; it does not verify the jar is present. Fail loud # here rather than letting `java -jar ` die with an opaque JSONDecodeError. jar = find_jar(_AST_EXTRACTION_JAR) From bc24b0d16af5e8063010e0681fba7169b13099f2 Mon Sep 17 00:00:00 2001 From: shellygr Date: Tue, 30 Jun 2026 21:59:09 +0300 Subject: [PATCH 5/6] Update certora_autosetup/setup/summary_resolver.py Co-authored-by: Naftali Goldstein <44599898+naftali-g@users.noreply.github.com> --- certora_autosetup/setup/summary_resolver.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora_autosetup/setup/summary_resolver.py b/certora_autosetup/setup/summary_resolver.py index 56dd2c6..6af4543 100644 --- a/certora_autosetup/setup/summary_resolver.py +++ b/certora_autosetup/setup/summary_resolver.py @@ -118,7 +118,7 @@ def _parse_ast_payload(stdout: str, returncode: int, stderr: str) -> Optional[di """ lines = stdout.splitlines() # Only LEADING diagnostic lines precede the JSON; never strip inside the payload. - while lines and (lines[0].startswith("Warning: ") or lines[0].startswith("Error: ")): + while lines and lines[0].startswith(("Warning: ", "Error: ")): lines.pop(0) body = "\n".join(lines).strip() # Empty stdout (or stdout that was nothing but diagnostics) means the jar gave us From ec34dd29e5588034d16cc14b3133be59b4d98e89 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Wed, 1 Jul 2026 02:56:51 +0300 Subject: [PATCH 6/6] nit --- certora_autosetup/setup/summary_resolver.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora_autosetup/setup/summary_resolver.py b/certora_autosetup/setup/summary_resolver.py index 56dd2c6..200a51b 100644 --- a/certora_autosetup/setup/summary_resolver.py +++ b/certora_autosetup/setup/summary_resolver.py @@ -130,7 +130,7 @@ def _parse_ast_payload(stdout: str, returncode: int, stderr: str) -> Optional[di except json.JSONDecodeError as exc: raise RuntimeError( f"{_AST_EXTRACTION_JAR} output was not JSON after stripping diagnostics " - f"(exit {returncode}): {exc}; stdout_head={stdout[:300]!r} stderr={stderr.strip()[:500]!r}" + f"(exit {returncode}): {exc}; stdout_head={stdout!r} stderr={stderr.strip()!r}" ) return payload if payload.get("ast") else None