diff --git a/models/default_llm_backend.py b/models/default_llm_backend.py index 00ebd07..151d285 100644 --- a/models/default_llm_backend.py +++ b/models/default_llm_backend.py @@ -1,6 +1,5 @@ """Default module for LLM-based generation.""" -# ruff: noqa # TODO: Vikram, please document. # Vikram would be best suited to document this class. @@ -23,9 +22,31 @@ class DefaultLlmBackend(LlmBackend): - """Encapsulate LLM-based generation logic.""" + """Encapsulate LLM-based generation logic. + + Wraps `litellm` to support both direct API access (via `LLM_API_KEY`) and + Google Cloud Vertex AI (via `VERTEX_AI_JSON`). Automatically retries on + transient errors and compacts the conversation when the context window is + exceeded. + + Attributes: + model (str): The litellm model string (e.g. `vertex_ai/claude-sonnet-4-6`). + max_tokens (int): Maximum tokens allowed in a single response. + api_key (str | None): API key for direct access; `None` when using Vertex AI. + vertex_credentials (str | None): JSON credentials for Vertex AI; `None` otherwise. + """ def __init__(self, model: str, use_vertex_api: bool): + """Create a new DefaultLlmBackend. + + Args: + model (str): The model name to use (e.g. `claude-sonnet-4-6`, `gpt-4o`). + use_vertex_api (bool): If True and `VERTEX_AI_JSON` is set, route requests + through Google Cloud Vertex AI using the credentials in that file. + + Raises: + ModelError: Raised when `model` is not a supported model name. + """ if use_vertex_api and "VERTEX_AI_JSON" in os.environ: litellm.vertex_location = "us-east5" with pathlib.Path(os.environ["VERTEX_AI_JSON"]).open(encoding="utf-8") as file: @@ -53,13 +74,23 @@ def send_messages( ) -> list[str]: """Return `top_k` sampled responses from the LLM for the given messages. + Retries up to 5 times on transient errors (rate limits, server errors, connection issues) + with a 10-second delay between attempts. On a context-window overflow, the conversation + is compacted and retried once. + Args: - messages (tuple[ConversationMessage, ...]): The conversation to send to the LLM. - temperature (float): The sampling temperature. Must be non-zero when `top_k > 1`. - top_k (int): The number of responses to sample. + messages (tuple[ConversationMessage, ...]): The conversation history to send. + temperature (float): Sampling temperature. Must be non-zero when `top_k > 1`. + top_k (int): Number of independent completions to request. Returns: - list[str]: The sampled responses. `len(returned) == top_k`. + list[str]: The text content of each completion, with `len(result) == top_k`. + + Raises: + GenerationError: Raised for unrecoverable API errors or invalid arguments. + ContextWindowExceededError: Raised when the context window is exceeded and the + conversation is already too short to compact further. + ModelError: Raised after 5 consecutive transient failures. """ if top_k < 1: raise GenerationError("top_k must be >= 1") @@ -165,9 +196,9 @@ def _send_with_retry( raise ModelError(msg) from e logger.warning(f"LLM Error {e}. Waiting 10 seconds and retrying") time.sleep(10) - except Exception as e: + except Exception as e: # noqa: BLE001 msg = f"LLM Error: {e}" - raise GenerationError(msg) + raise GenerationError(msg) # noqa: B904 @staticmethod def get_instance(model_name: str, use_vertex_api: bool) -> LlmBackend: diff --git a/test/util/test_spec_syntax_fixer.py b/test/util/test_spec_syntax_fixer.py index da1d966..3fdabb1 100644 --- a/test/util/test_spec_syntax_fixer.py +++ b/test/util/test_spec_syntax_fixer.py @@ -13,7 +13,7 @@ CLAUSES_WITH_ILLEGAL_ARRAY_RANGES_TO_FIXED_CLAUSES = { "__CPROVER_assigns(arr[lo...hi], a, arr2[i])": "__CPROVER_assigns(*arr, a, arr2[i])", "__CPROVER_assigns(a, arr[1..2], arr2[i])": "__CPROVER_assigns(a, *arr, arr2[i])", - "__CPROVER_assigns(a, arr2[i], arr[lo+2:3])": "__CPROVER_assigns(a, arr2[i], *arr)" + "__CPROVER_assigns(a, arr2[i], arr[lo+2:3])": "__CPROVER_assigns(a, arr2[i], *arr)", } # These are some examples of specifications that contain ellipses (...), which are illegal. @@ -52,16 +52,19 @@ def test_fix_illegal_ellipses() -> None: # We only care about the postconditions. assert fixed_spec.postconditions == ["__CPROVER_assigns(a, b, c)"] + def test_fix_illegal_array_ranges_with_unrelated_assigns_targets() -> None: for illegal_clause, fixed_clause in CLAUSES_WITH_ILLEGAL_ARRAY_RANGES_TO_FIXED_CLAUSES.items(): - spec_with_illegal_clause = FunctionSpecification(preconditions=[], postconditions=[illegal_clause]) + spec_with_illegal_clause = FunctionSpecification( + preconditions=[], postconditions=[illegal_clause] + ) fixed_spec = fix_syntax(spec_with_illegal_clause) assert fixed_spec.postconditions == [fixed_clause] def test_fix_multiple_illegal_ellipses() -> None: - spec_with_multiple_illegal_ellipses = FunctionSpecification(preconditions=[], postconditions=["__CPROVER_assigns(a, b, ..., c, ..., d)"]) + spec_with_multiple_illegal_ellipses = FunctionSpecification( + preconditions=[], postconditions=["__CPROVER_assigns(a, b, ..., c, ..., d)"] + ) fixed_spec = fix_syntax(spec_with_multiple_illegal_ellipses) assert fixed_spec.postconditions == ["__CPROVER_assigns(a, b, c, d)"] - - diff --git a/translation/ast/cbmc_ast.py b/translation/ast/cbmc_ast.py index da2dc11..70af672 100644 --- a/translation/ast/cbmc_ast.py +++ b/translation/ast/cbmc_ast.py @@ -6,16 +6,19 @@ # Ideally we'd like to type check this file, but Lark does not yet support type annotations. # mypy: ignore-errors -# ruff: noqa +# ruff: noqa: D101, D102, N802, DOC502 from __future__ import annotations + import sys from abc import ABC, abstractmethod from dataclasses import dataclass -from typing import Any, Protocol +from typing import TYPE_CHECKING, Any, Protocol from lark import Transformer, ast_utils, v_args -from lark.tree import Meta + +if TYPE_CHECKING: + from lark.tree import Meta class Mutable(Protocol): diff --git a/util/text_util.py b/util/text_util.py index 03eee55..9451665 100644 --- a/util/text_util.py +++ b/util/text_util.py @@ -29,8 +29,12 @@ def prepend_line_numbers(lines: list[str], start: int, end: int) -> list[tuple[s if len(lines) != end - start: msg = ( f"Mismatch between length of lines ({len(lines)}) and " - f"range of lines (start = {start}, end = {end})" + f"range of lines (start = {start}, end (exclusive) = {end}). Lines = \n" ) + lineno = 1 + for line in lines: + msg += f"{lineno}\t{line}\n" + lineno = lineno + 1 raise RuntimeError(msg) line_number_width = len(str(end)) return [(f"{str(n).ljust(line_number_width)}", lines[n - start]) for n in range(start, end)]