Code review improvements

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:

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)"]
-
-

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):

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)]