Open
Conversation
Contributor
📝 WalkthroughWalkthroughAdds a public CbmcAst.to_string() API and a default negate() on the CBMC AST base, implements to_string() across many AST node classes, introduces LogicalBinOp and related utilities, and refines negate() behavior for logical and comparison nodes. Adds _to_str helper and dereference-subexpression support on PtrMemberOp. Introduces SpecificationVariantFactory and four specification transformations (MovePreconditionsToAssignsAndEnsures, RemovePreconditions, InferNonNullPreconditionsFromEnsures, MinimizeConditionalAssigns), updates package exports to expose them, and adds unit tests for the new transformations. Possibly related PRs
Suggested reviewers
🚥 Pre-merge checks | ❌ 1❌ Failed checks (1 warning)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
Contributor
There was a problem hiding this comment.
Actionable comments posted: 6
🤖 Fix all issues with AI agents
In `@test/util/test_spec_transformer.py`:
- Around line 18-34: Add a unit test that covers negation of non-comparison
expressions by calling transformer.move_preconditions_to_ensures with a
FunctionSpecification containing a precondition like
"__CPROVER_requires(valid(pp))" (a CallOp) and asserting the resulting
postcondition contains the negated form "!valid(pp)" in the disjunction;
reference the existing test function name
test_move_preconditions_to_ensures_disjunctions (or create a new test e.g.
test_negate_non_comparison_expressions) and ensure the assertion checks that
_negate produces a prefix negation for CallOp inputs rather than applying
comparison-specific logic.
- Around line 6-16: Remove the stray blank line inside the preconditions list in
the test function
test_move_preconditions_to_ensures_returns_unchanged_specs_if_no_ensures_clause:
edit the FunctionSpecification instance assigned to spec_without_ensures so the
preconditions list has no blank line between the opening bracket and the first
string element (the "__CPROVER_requires(...)" entries), keeping the same items
and formatting otherwise.
In `@util/spec_transformer.py`:
- Around line 31-35: The _parser variable is a class-level constant that
constructs Parser(...) at import time causing brittle import-time file reads;
change initialization to be lazy by moving creation of
Parser(path_to_grammar_defn="translation/grammar/cbmc.txt", start="cbmc_clause",
transformer=ToAst()) into the SpecTransformer.__init__ (or implement a
`@property/classproperty` that creates and caches the Parser on first access) so
imports no longer read the grammar file; ensure references to _parser inside
methods use the instance attribute (self._parser) or the lazy accessor and
preserve the same Parser parameters and ToAst transformer.
- Around line 78-82: The code silently drops parsed preconditions that are not
instances of RequiresClause (created via self._parser.parse) which can remove
preconditions or lead to _apply_logical_op receiving an empty list; update
spec_transformer.py to validate the result of self._parser.parse for each item
in preconditions (and analogously for postconditions if applicable), and either
raise a descriptive error or emit a warning (using the module logger) when a
clause is not a RequiresClause instead of filtering it out; ensure this
validation occurs before building precondition_exprs so _apply_logical_op never
receives an unexpected empty list and reference the variables/functions:
preconditions, postconditions, self._parser.parse, RequiresClause,
precondition_exprs, and _apply_logical_op.
- Around line 219-220: The catch-all branch in _negate currently returns the
input expression unchanged, which silently skips negation for unmatched node
types (e.g., CallOp, Name, ForallExpr, IndexOp); change the default branch in
_negate to wrap the expression in a NotOp (i.e., return NotOp(expr)) so any
unhandled expression is properly negated—update references in _negate and ensure
NotOp is used consistently with existing negation handling.
- Around line 174-189: The _apply_logical_op function currently mutates the
input list and crashes on an empty list; change it to be non-destructive and
handle empty exprs by returning a sensible default or raising a clear error.
Specifically, in _apply_logical_op(exprs: list[CBMCAst], logical_op: type[AndOp
| OrOp]) avoid using pop() on exprs (which mutates the caller) and instead
operate on a shallow copy or use functools.reduce to fold the list; first check
if exprs is empty and either return an explicit empty-value sentinel or raise a
ValueError with context, otherwise reduce the sequence into a single CBMCAst
using logical_op (e.g., reduce with a lambda that constructs logical_op(left=a,
right=b)). Ensure references to _apply_logical_op, exprs, and logical_op are
updated accordingly.
Contributor
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 Fix all issues with AI agents
In `@test/util/test_spec_transformer.py`:
- Line 28: Remove the debug print statement printing actual_transformed_spec
from the test file; locate the stray print(actual_transformed_spec) in
test/util/test_spec_transformer.py (inside the test function that constructs
actual_transformed_spec) and delete it so the test contains no side-effectful
prints (keep existing assertions untouched).
Contributor
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 Fix all issues with AI agents
In `@test/util/test_spec_transformer.py`:
- Line 36: Rename the test function to match the sibling naming pattern: change
test_move_preconditions_returns_unchanged_spec_if_no_assigns to
test_move_preconditions_to_assigns_returns_unchanged_spec_if_no_assigns so it
consistently references the method under test (move_preconditions_to_assigns)
and aligns with test_move_preconditions_to_assigns_conditional.
mernst
requested changes
Feb 19, 2026
Contributor
There was a problem hiding this comment.
Actionable comments posted: 4
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@translation/ast/cbmc_ast.py`:
- Around line 19-35: Several AST node classes (Name, Number, Bool, StringLit,
MemberOp, PtrMemberOp, IndexOp, AddrOp, DerefOp, NegOp, PosOp, Old, ReturnValue)
lack a negate() implementation causing NotImplementedError when AndOp.negate()
or OrOp.negate() recursively calls negate(); implement negate() on each of these
classes to return a NotOp wrapping self (matching CallOp.negate() behavior) so
unsupported/atomic expressions are negated safely, ensuring
AndOp.negate()/OrOp.negate() can recurse without crashes.
In `@util/spec_transformer.py`:
- Around line 131-138: preconditions are parsed into clause objects and then you
call clause.expr.negate() in negated_precondition_exprs which will raise
NotImplementedError for expression node types that don't implement negate (e.g.
Name, MemberOp, IndexOp per cbmc_ast.py); instead, implement a safe negation
helper (or use an AST-level wrapper) that transforms expressions into their
logical negation by pattern-matching on node types (handle Name, MemberOp,
IndexOp, BoolOp, Comparison, etc.) and fallback to wrapping with a NotOp for
unsupported nodes, and update the code that builds negated_precondition_exprs to
call that helper (referencing preconditions, negated_precondition_exprs, and
RequiresClause to locate the spot to change).
- Line 26: The __init__ method in class SpecTransformer is missing an explicit
return type annotation; update the definition of __init__ (the constructor) to
include the return type annotation "-> None" so it becomes def __init__(self) ->
None: to satisfy Ruff ANN204 and make the signature explicit across
util/spec_transformer.py.
- Around line 157-167: The private helper _get_assigns_clauses in
util/spec_transformer.py is unused; either remove the method entirely or, if you
plan to keep it, add a clear TODO/docstring explaining its intended future use
and why it's retained; locate the function named _get_assigns_clauses (which
references FunctionSpecification, Assigns, and self._parser.parse) and either
delete its definition or replace its docstring with a TODO explaining the
planned purpose and expected callers.
Contributor
There was a problem hiding this comment.
Actionable comments posted: 2
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
translation/ast/cbmc_ast.py (1)
411-416: 🧹 Nitpick | 🔵 Trivial
Quantifieris a concrete@dataclasswith noto_string()override – direct instantiation silently inheritsNotImplementedError.
ForallExprandExistsExprboth implementto_string(), butQuantifieritself is a concrete dataclass that inherits the baseCBMCAst.to_string()which raisesNotImplementedError. Nothing preventsQuantifier(decl=..., range_expr=..., expr=...)from being constructed directly. Consider marking it abstract:♻️ Proposed refactor
+from abc import ABC + `@dataclass` -class Quantifier(CBMCAst): +class Quantifier(ABC, CBMCAst): decl: QuantifierDecl range_expr: Any expr: Any kind: str = ""🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@translation/ast/cbmc_ast.py` around lines 411 - 416, Quantifier is a concrete dataclass but relies on CBMCAst.to_string() which raises NotImplementedError, so prevent silent instantiation by making Quantifier abstract or providing a default to_string; update the class definition for Quantifier to either (a) inherit from abc.ABC (or CBMCAst if it already is abstract) and declare to_string as an abstractmethod so instantiating Quantifier is disallowed, or (b) implement a concrete to_string in Quantifier that delegates to subclass behavior (used by ForallExpr/ExistsExpr) to avoid the NotImplementedError; reference the Quantifier class, CBMCAst.to_string, and the existing ForallExpr/ExistsExpr implementations when applying the change.
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@translation/ast/cbmc_ast.py`:
- Around line 344-350: PtrMemberOp currently types attr as str which conflicts
with the runtime check and usage in to_string (it expects a Name/CBMCAst);
change the annotation from attr: str to attr: CBMCAst (or a more specific Name
type if preferred) so it matches MemberOp.attr and the isinstance(self.attr,
Name) guard in to_string and update any imports/typing references accordingly.
In `@util/spec_transformer.py`:
- Around line 75-94: precondition_exprs is being combined eagerly by calling
self._apply_logical_op(precondition_exprs, AndOp) even when no Assigns clause
exists; change this to compute the conjunction lazily by deferring the call
until you encounter the first Assigns in postconditions (e.g., compute
conjunction_of_preconditions_exprs only when is_assigns_clause_updated would
become True), then assign that result to clause.condition, set
is_assigns_clause_updated, and continue collecting updated_postconditions;
ensure behavior still returns FunctionSpecification(preconditions=[],
postconditions=updated_postconditions) when an Assigns was updated, otherwise
return the original spec.
---
Outside diff comments:
In `@translation/ast/cbmc_ast.py`:
- Around line 411-416: Quantifier is a concrete dataclass but relies on
CBMCAst.to_string() which raises NotImplementedError, so prevent silent
instantiation by making Quantifier abstract or providing a default to_string;
update the class definition for Quantifier to either (a) inherit from abc.ABC
(or CBMCAst if it already is abstract) and declare to_string as an
abstractmethod so instantiating Quantifier is disallowed, or (b) implement a
concrete to_string in Quantifier that delegates to subclass behavior (used by
ForallExpr/ExistsExpr) to avoid the NotImplementedError; reference the
Quantifier class, CBMCAst.to_string, and the existing ForallExpr/ExistsExpr
implementations when applying the change.
Comment on lines
+344
to
+350
| class PtrMemberOp(CBMCAst): | ||
| value: Any | ||
| attr: str | ||
|
|
||
| def to_string(self) -> str: | ||
| attr = self.attr.name if isinstance(self.attr, Name) else str(self.attr) | ||
| return f"{_to_str(self.value)}->{attr}" |
Contributor
There was a problem hiding this comment.
PtrMemberOp.attr: str type annotation contradicts its own isinstance guard.
The to_string() implementation checks isinstance(self.attr, Name), which would always be False if attr were actually a str. In practice, _ToAst.NAME converts all NAME grammar tokens into Name objects, so attr arrives as a Name node at runtime, not a plain string. Compare MemberOp.attr: CBMCAst which is correctly typed. The annotation should be corrected:
📝 Proposed fix
`@dataclass`
class PtrMemberOp(CBMCAst):
value: Any
- attr: str
+ attr: Any🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@translation/ast/cbmc_ast.py` around lines 344 - 350, PtrMemberOp currently
types attr as str which conflicts with the runtime check and usage in to_string
(it expects a Name/CBMCAst); change the annotation from attr: str to attr:
CBMCAst (or a more specific Name type if preferred) so it matches MemberOp.attr
and the isinstance(self.attr, Name) guard in to_string and update any
imports/typing references accordingly.
…erification into yoo/spec-transformer
Contributor
There was a problem hiding this comment.
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Duplicate comments:
In `@util/spec_transformer.py`:
- Line 80: conjunction_of_preconditions_exprs and
disjunction_of_negated_precondition_exprs are being computed eagerly even when
no Assigns/EnsuresClause will be processed; move their computation inside the
postcondition loop so they are only built when a relevant clause is present.
Specifically, delay calling self._apply_logical_op(precondition_exprs, AndOp)
(conjunction_of_preconditions_exprs) and
self._apply_logical_op(negated_precondition_exprs, OrOp)
(disjunction_of_negated_precondition_exprs) until after you detect an
Assigns/EnsuresClause in the loop that needs them, and reference those variables
only after computing them to avoid wasted work.
…erification into yoo/spec-transformer
Contributor
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@util/spec_transformer.py`:
- Around line 130-137: Move the eager computation of negated_precondition_exprs
and disjunction_of_negated_precondition_exprs into the branch that processes
postconditions so we only compute them when an EnsuresClause is present: instead
of building negated_precondition_exprs and calling clause.expr.negate() for all
RequiresClause instances up-front, detect if the current postcondition being
handled is an EnsuresClause and then call clause.expr.negate() and
_apply_logical_op(…, OrOp) as needed; update the logic that references
negated_precondition_exprs/disjunction_of_negated_precondition_exprs to use the
lazily-computed values within the postcondition loop.
---
Duplicate comments:
In `@util/spec_transformer.py`:
- Around line 83-87: The loop re-computes
self._apply_logical_op(precondition_exprs, AndOp) for every Assigns clause,
wasting allocations; before iterating postconditions compute and cache the
conjunction in a local variable (e.g., assigns_condition = None then assign it
on first use) and reuse it inside the loop when isinstance(clause, Assigns),
still setting clause.condition and is_assigns_clause_updated as before and
appending clause.to_string() to updated_postconditions.
Comment on lines
+130
to
+137
| preconditions = [self._parser.parse(clause) for clause in spec.preconditions] | ||
| postconditions = [self._parser.parse(clause) for clause in spec.postconditions] | ||
| negated_precondition_exprs = [ | ||
| clause.expr.negate() for clause in preconditions if isinstance(clause, RequiresClause) | ||
| ] | ||
| disjunction_of_negated_precondition_exprs = self._apply_logical_op( | ||
| negated_precondition_exprs, OrOp | ||
| ) |
Contributor
There was a problem hiding this comment.
🧹 Nitpick | 🔵 Trivial
Negation and disjunction computed eagerly before the postconditions loop.
negated_precondition_exprs and disjunction_of_negated_precondition_exprs (lines 132–137) are built unconditionally before inspecting postconditions. If no EnsuresClause is present, all negate() calls and AST allocations are wasted. This is the same laziness concern previously raised for move_preconditions_to_assigns, and can be addressed by moving the computation inside the loop:
♻️ Proposed fix
- negated_precondition_exprs = [
- clause.expr.negate() for clause in preconditions if isinstance(clause, RequiresClause)
- ]
- disjunction_of_negated_precondition_exprs = self._apply_logical_op(
- negated_precondition_exprs, OrOp
- )
-
updated_postconditions = []
is_ensures_clause_updated = False
+ disjunction_of_negated_precondition_exprs: CBMCAst | None = None
for clause in postconditions:
if isinstance(clause, EnsuresClause):
+ if disjunction_of_negated_precondition_exprs is None:
+ negated_precondition_exprs = [
+ c.expr.negate()
+ for c in preconditions
+ if isinstance(c, RequiresClause)
+ ]
+ disjunction_of_negated_precondition_exprs = self._apply_logical_op(
+ negated_precondition_exprs, OrOp
+ )
updated_ensures_expr = self._apply_logical_op(
[disjunction_of_negated_precondition_exprs, clause.expr], OrOp
)🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@util/spec_transformer.py` around lines 130 - 137, Move the eager computation
of negated_precondition_exprs and disjunction_of_negated_precondition_exprs into
the branch that processes postconditions so we only compute them when an
EnsuresClause is present: instead of building negated_precondition_exprs and
calling clause.expr.negate() for all RequiresClause instances up-front, detect
if the current postcondition being handled is an EnsuresClause and then call
clause.expr.negate() and _apply_logical_op(…, OrOp) as needed; update the logic
that references
negated_precondition_exprs/disjunction_of_negated_precondition_exprs to use the
lazily-computed values within the postcondition loop.
Contributor
There was a problem hiding this comment.
Actionable comments posted: 6
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@specifications/__init__.py`:
- Line 5: __all__ is not sorted; reorder the list so entries are in
lexicographic order: update __all__ to ["LlmSpecificationGenerator",
"SpecificationVariantFactory", "extract_spec_from_response"] so the symbols
LlmSpecificationGenerator, SpecificationVariantFactory and
extract_spec_from_response appear sorted.
In `@specifications/variants/specification_variant_factory.py`:
- Around line 23-32: The get_variants method is returning transformations that
may be identical to the original spec (because Transformation.apply can return
the same spec), causing duplicate verification; update get_variants (in
specification_variant_factory.py) to filter out any resulting
FunctionSpecification equal to the input spec by using
FunctionSpecification.__eq__ (i.e., only include variants where transformed_spec
!= spec) when building the returned tuple from self._transformations.apply
calls.
In `@specifications/variants/transformations/__init__.py`:
- Line 4: The __all__ export list in
specifications/variants/transformations/__init__.py is unsorted; update the
__all__ assignment so the identifiers are in alphabetical order (e.g.,
["MovePreconditionsToAssignsAndEnsures", "SpecificationTransformation"]) to
satisfy Ruff RUF022; edit the __all__ variable in that module to contain the
sorted symbol names.
In `@specifications/variants/transformations/specification_transformation.py`:
- Around line 29-32: The docstring for the method that returns a
FunctionSpecification contains a copy-paste error: replace the phrase "applying
this specification to the given specification" with "applying this
transformation to the given specification" (i.e., change "this specification" to
"this transformation") in the Returns section of the method that produces a
FunctionSpecification (the apply/transform method in SpecificationTransformation
or similar in specification_transformation.py) so it reads: "The result of
applying this transformation to the given specification."
- Around line 16-19: The class currently only annotates _parser which doesn't
guarantee an attribute at runtime; change the design to require an abstract
property named parser (or _parser consistently) by adding a `@property` decorated
`@abstractmethod` on the class (so subclasses must implement it) and update the
class docstring to refer to the same attribute name you choose (parser vs
_parser); ensure _parse_specification and any other methods access the property
(parser) rather than relying on a bare annotated name so missing implementations
are caught at subclass instantiation time.
In
`@test/specifications/transformations/test_move_preconditions_to_assigns_and_ensures.py`:
- Around line 39-56: Add two unit tests for transformation.apply(): (1) a test
using a FunctionSpecification with preconditions=[] and at least one
"__CPROVER_ensures(...)" to exercise the early-return guard in apply() (the "if
not precondition_exprs: return specification" path) and assert the returned spec
equals the input spec; (2) a test where postconditions include an
"__CPROVER_assigns" that already has a condition (e.g.,
"__CPROVER_assigns(p->valid : p->buf)") and preconditions contains a requires
(e.g., "p != NULL") to exercise the branch that ANDs post_ast.condition with the
new precondition conjunction, then assert preconditions become empty and the
resulting assigns condition string contains both the original condition
(p->valid) and the new precondition (p != NULL).
| from .variants.specification_variant_factory import SpecificationVariantFactory | ||
|
|
||
| __all__ = ["LlmSpecificationGenerator", "extract_spec_from_response"] No newline at end of file | ||
| __all__ = ["LlmSpecificationGenerator", "extract_spec_from_response", "SpecificationVariantFactory"] No newline at end of file |
Contributor
There was a problem hiding this comment.
__all__ is not sorted (Ruff RUF022).
✏️ Proposed fix
-__all__ = ["LlmSpecificationGenerator", "extract_spec_from_response", "SpecificationVariantFactory"]
+__all__ = ["LlmSpecificationGenerator", "SpecificationVariantFactory", "extract_spec_from_response"]🧰 Tools
🪛 Ruff (0.15.1)
[warning] 5-5: __all__ is not sorted
Apply an isort-style sorting to __all__
(RUF022)
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@specifications/__init__.py` at line 5, __all__ is not sorted; reorder the
list so entries are in lexicographic order: update __all__ to
["LlmSpecificationGenerator", "SpecificationVariantFactory",
"extract_spec_from_response"] so the symbols LlmSpecificationGenerator,
SpecificationVariantFactory and extract_spec_from_response appear sorted.
Comment on lines
+23
to
+32
| def get_variants(self, spec: FunctionSpecification) -> tuple[FunctionSpecification, ...]: | ||
| """Return the variants of the given specification. | ||
|
|
||
| Args: | ||
| spec (FunctionSpecification): The specifications for which to generate variants. | ||
|
|
||
| Returns: | ||
| tuple[FunctionSpecification, ...]: The variants of the given specification. | ||
| """ | ||
| return tuple(transformation.apply(spec) for transformation in self._transformations) |
Contributor
There was a problem hiding this comment.
get_variants can return the original spec unchanged, causing duplicate verification runs.
apply() explicitly returns the input spec object when there are no postconditions or no precondition expressions. get_variants forwards this directly, so callers that iterate over the returned variants and run verification would redo exactly the same check that already failed on the original spec.
Since FunctionSpecification implements __eq__, the fix is a one-line filter:
🐛 Proposed fix
def get_variants(self, spec: FunctionSpecification) -> tuple[FunctionSpecification, ...]:
...
- return tuple(transformation.apply(spec) for transformation in self._transformations)
+ return tuple(
+ result
+ for transformation in self._transformations
+ if (result := transformation.apply(spec)) != spec
+ )🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@specifications/variants/specification_variant_factory.py` around lines 23 -
32, The get_variants method is returning transformations that may be identical
to the original spec (because Transformation.apply can return the same spec),
causing duplicate verification; update get_variants (in
specification_variant_factory.py) to filter out any resulting
FunctionSpecification equal to the input spec by using
FunctionSpecification.__eq__ (i.e., only include variants where transformed_spec
!= spec) when building the returned tuple from self._transformations.apply
calls.
| from .specification_transformation import SpecificationTransformation | ||
| from .move_preconditions_to_assigns_and_ensures import MovePreconditionsToAssignsAndEnsures | ||
|
|
||
| __all__ = ["SpecificationTransformation", "MovePreconditionsToAssignsAndEnsures"] No newline at end of file |
Contributor
There was a problem hiding this comment.
__all__ is not sorted (Ruff RUF022).
✏️ Proposed fix
-__all__ = ["SpecificationTransformation", "MovePreconditionsToAssignsAndEnsures"]
+__all__ = ["MovePreconditionsToAssignsAndEnsures", "SpecificationTransformation"]📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| __all__ = ["SpecificationTransformation", "MovePreconditionsToAssignsAndEnsures"] | |
| __all__ = ["MovePreconditionsToAssignsAndEnsures", "SpecificationTransformation"] |
🧰 Tools
🪛 Ruff (0.15.1)
[warning] 4-4: __all__ is not sorted
Apply an isort-style sorting to __all__
(RUF022)
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@specifications/variants/transformations/__init__.py` at line 4, The __all__
export list in specifications/variants/transformations/__init__.py is unsorted;
update the __all__ assignment so the identifiers are in alphabetical order
(e.g., ["MovePreconditionsToAssignsAndEnsures", "SpecificationTransformation"])
to satisfy Ruff RUF022; edit the __all__ variable in that module to contain the
sorted symbol names.
Comment on lines
+16
to
+19
| parser (Parser[CBMCAst]): A parser for CBMC ASTs. | ||
| """ | ||
|
|
||
| _parser: Parser[CBMCAst] |
Contributor
There was a problem hiding this comment.
🧹 Nitpick | 🔵 Trivial
Enforce _parser initialization via an abstract property — bare annotation gives no runtime guarantee.
_parser: Parser[CBMCAst] at the class level only registers the name in __annotations__; it does not create any attribute. A subclass that neglects to set self._parser in __init__ will crash with AttributeError the first time _parse_specification is called. Additionally, the class docstring names the attribute parser while the actual identifier is _parser.
♻️ Suggested refactor — abstract property + docstring fix
-class SpecificationTransformation(ABC):
- """Represent a transformation of a specification.
-
- Attributes:
- parser (Parser[CBMCAst]): A parser for CBMC ASTs.
- """
-
- _parser: Parser[CBMCAst]
+class SpecificationTransformation(ABC):
+ """Represent a transformation of a specification.
+
+ Attributes:
+ _parser (Parser[CBMCAst]): A parser for CBMC ASTs.
+ """
+
+ `@property`
+ `@abstractmethod`
+ def _parser(self) -> "Parser[CBMCAst]":
+ """Return the parser used to parse CBMC ASTs."""
+ ...As per the Python docs, @property @abstractmethod`` is the canonical way to enforce that subclasses provide a concrete implementation of an attribute, preventing instantiation of any subclass that omits it.
📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| parser (Parser[CBMCAst]): A parser for CBMC ASTs. | |
| """ | |
| _parser: Parser[CBMCAst] | |
| _parser (Parser[CBMCAst]): A parser for CBMC ASTs. | |
| """ | |
| `@property` | |
| `@abstractmethod` | |
| def _parser(self) -> "Parser[CBMCAst]": | |
| """Return the parser used to parse CBMC ASTs.""" | |
| ... |
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@specifications/variants/transformations/specification_transformation.py`
around lines 16 - 19, The class currently only annotates _parser which doesn't
guarantee an attribute at runtime; change the design to require an abstract
property named parser (or _parser consistently) by adding a `@property` decorated
`@abstractmethod` on the class (so subclasses must implement it) and update the
class docstring to refer to the same attribute name you choose (parser vs
_parser); ensure _parse_specification and any other methods access the property
(parser) rather than relying on a bare annotated name so missing implementations
are caught at subclass instantiation time.
Comment on lines
+39
to
+56
| def test_move_preconditions_to_ensures_disjunctions_and_assigns_conditions(): | ||
| spec_with_preconditions = FunctionSpecification( | ||
| preconditions=[ | ||
| "__CPROVER_requires(pp != NULL)", | ||
| "__CPROVER_requires(pp->p != NULL)", | ||
| "__CPROVER_requires(pp->p->buf != NULL)", | ||
| ], | ||
| postconditions=["__CPROVER_ensures(pp->p->buf[0] == 0)", "__CPROVER_assigns(pp->p->buf)"], | ||
| ) | ||
| actual_transformed_spec = transformation.apply(spec_with_preconditions) | ||
| expected_transformed_spec = FunctionSpecification( | ||
| preconditions=[], | ||
| postconditions=[ | ||
| "__CPROVER_ensures(((((pp == NULL) || (pp->p == NULL)) || (pp->p->buf == NULL)) || (pp->p->buf[0] == 0)))", | ||
| "__CPROVER_assigns((((pp != NULL) && (pp->p != NULL)) && (pp->p->buf != NULL)) : pp->p->buf)", | ||
| ], | ||
| ) | ||
| assert actual_transformed_spec == expected_transformed_spec |
Contributor
There was a problem hiding this comment.
🧹 Nitpick | 🔵 Trivial
Two branches in apply() lack test coverage.
-
No preconditions, with postconditions — the
if not precondition_exprs: return specificationguard (line 59 in the transformation) is never exercised. A spec with an empty preconditions list and at least one__CPROVER_ensureswould cover it. -
Assignswith a pre-existing condition — theif post_ast.condition:branch (line 79–80 in the transformation) that ANDs the existing assigns condition with the new precondition conjunction is not tested. The current test uses a bare__CPROVER_assigns(pp->p->buf)which has no condition.
🧪 Suggested additional tests
def test_move_preconditions_returns_unchanged_if_no_preconditions():
spec = FunctionSpecification(
preconditions=[],
postconditions=["__CPROVER_ensures(x == 0)"],
)
assert transformation.apply(spec) == spec
def test_move_preconditions_combines_with_existing_assigns_condition():
spec = FunctionSpecification(
preconditions=["__CPROVER_requires(p != NULL)"],
postconditions=["__CPROVER_assigns(p->valid : p->buf)"],
)
result = transformation.apply(spec)
# Expect condition to be: (p->valid && (p != NULL))
assert result.preconditions == []
assert len(result.postconditions) == 1
assert "p->valid" in result.postconditions[0]
assert "p != NULL" in result.postconditions[0]🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In
`@test/specifications/transformations/test_move_preconditions_to_assigns_and_ensures.py`
around lines 39 - 56, Add two unit tests for transformation.apply(): (1) a test
using a FunctionSpecification with preconditions=[] and at least one
"__CPROVER_ensures(...)" to exercise the early-return guard in apply() (the "if
not precondition_exprs: return specification" path) and assert the returned spec
equals the input spec; (2) a test where postconditions include an
"__CPROVER_assigns" that already has a condition (e.g.,
"__CPROVER_assigns(p->valid : p->buf)") and preconditions contains a requires
(e.g., "p != NULL") to exercise the branch that ANDs post_ast.condition with the
new precondition conjunction, then assert preconditions become empty and the
resulting assigns condition string contains both the original condition
(p->valid) and the new precondition (p != NULL).
Contributor
There was a problem hiding this comment.
Actionable comments posted: 5
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@specifications/variants/specification_variant_factory.py`:
- Line 35: The current return uses tuple(variants) where variants is a set,
which yields non-deterministic ordering; change it to produce a deterministic
ordering by sorting before converting to a tuple (e.g., use sorted(variants,
key=str) or another stable key appropriate for the variant objects) so the
return value from the line returning tuple(variants) is reproducible across
runs.
In
`@specifications/variants/transformations/move_preconditions_to_assigns_and_ensures.py`:
- Around line 28-32: The parser initialization for Parser(...,
start="cbmc_clause", transformer=ToAst()) is duplicated in
MovePreconditionsToAssignsAndEnsures.__init__ (and noted in
RemovePreconditions.__init__); move this construction into the base class
SpecificationTransformation.__init__ so both subclasses reuse a single
self._parser setup, then remove the Parser(...) block from
MovePreconditionsToAssignsAndEnsures.__init__ (and RemovePreconditions.__init__)
and ensure they simply rely on the inherited self._parser; reference Parser,
ToAst, self._parser, MovePreconditionsToAssignsAndEnsures.__init__,
RemovePreconditions.__init__, and SpecificationTransformation.__init__ when
making the change.
In `@specifications/variants/transformations/remove_preconditions.py`:
- Line 52: The inline comment in remove_preconditions.py contains a typo:
replace the word "postcondition" with "precondition" in the sentence "(i.e.,
facts assumed in a prior postcondition may be used in the next)" so it reads
"(i.e., facts assumed in a prior precondition may be used in the next)"; locate
the comment in the module (around the block explaining precondition handling)
and update the wording accordingly.
- Around line 17-21: Both RemovePreconditions.__init__ and
MovePreconditionsToAssignsAndEnsures.__init__ duplicate construction of the
Parser (Parser(path_to_grammar_defn="translation/grammar/cbmc.txt",
start="cbmc_clause", transformer=ToAst())); move that Parser initialization into
SpecificationTransformation.__init__ so subclasses inherit it: add self._parser
= Parser(...) to SpecificationTransformation.__init__ (using the same
path_to_grammar_defn, start and transformer symbols) and remove the identical
self._parser assignments from RemovePreconditions.__init__ and
MovePreconditionsToAssignsAndEnsures.__init__ so there’s a single source of
truth for the parser.
- Around line 44-71: Remove the ValueError by adding the same early-return guard
used in MovePreconditionsToAssignsAndEnsures.apply: in
RemovePreconditions.apply, check if specification.postconditions is empty and if
so return [specification] immediately; this prevents constructing
FunctionSpecification with both preconditions=[] and postconditions=[] when
generating the single-removed and all-removed variants, preserving valid inputs
and avoiding the crash in FunctionSpecification.__init__.
---
Duplicate comments:
In `@specifications/variants/specification_variant_factory.py`:
- Around line 32-35: The get_variants method currently accumulates
transformation.apply(spec) results into variants but does not exclude the
original spec when a transformation is a no-op; update the method (the loop
using self._transformations and the return that builds tuple(variants)) to
remove the original spec from the collected variants before returning (e.g.,
discard or filter out any item equal to spec) so only true variants are
returned.
In `@specifications/variants/transformations/__init__.py`:
- Line 5: The __all__ list is not alphabetically sorted causing a Ruff RUF022
lint failure; update the __all__ variable to list the export names in sorted
order by changing it from ["SpecificationTransformation",
"MovePreconditionsToAssignsAndEnsures", "RemovePreconditions"] to
["MovePreconditionsToAssignsAndEnsures", "RemovePreconditions",
"SpecificationTransformation"] so the exported symbols are alphabetized.
In `@specifications/variants/transformations/specification_transformation.py`:
- Around line 16-19: The class-level bare annotation _parser: Parser[CBMCAst] is
unresolved and the docstring parameter name 'parser' mismatches; change the
docstring to refer to '_parser' (or remove the incorrect 'parser' entry) and
make the annotation concrete by either initializing it (e.g., set _parser = None
and use Optional[Parser[CBMCAst]]) or move the annotation/assignment into the
__init__ to enforce runtime presence; update references to use _parser
consistently and import typing.Optional or use from __future__ import
annotations if needed.
- Around line 29-32: Update the Returns docstring in
specification_transformation.py for the method that returns
list[FunctionSpecification] so the phrase "applying this specification to the
given specification" is corrected to "applying this transformation to the given
specification"; locate the Returns block (the one annotating
list[FunctionSpecification]) and replace the duplicated word "specification"
with "transformation" to accurately describe the method's behavior.
| variants = set() | ||
| for transformation in self._transformations: | ||
| variants.update(transformation.apply(spec)) | ||
| return tuple(variants) |
Contributor
There was a problem hiding this comment.
tuple(variants) has non-deterministic ordering across runs.
variants is a set; due to Python's PYTHONHASHSEED randomisation, tuple(variants) produces a different ordering on each interpreter invocation. If callers depend on a stable iteration order (e.g., prioritising variants), this will behave non-reproducibly.
♻️ Proposed fix — sort before converting to tuple
- return tuple(variants)
+ return tuple(
+ sorted(variants, key=lambda s: (s.preconditions, s.postconditions))
+ )🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@specifications/variants/specification_variant_factory.py` at line 35, The
current return uses tuple(variants) where variants is a set, which yields
non-deterministic ordering; change it to produce a deterministic ordering by
sorting before converting to a tuple (e.g., use sorted(variants, key=str) or
another stable key appropriate for the variant objects) so the return value from
the line returning tuple(variants) is reproducible across runs.
Comment on lines
+17
to
+21
| self._parser = Parser( | ||
| path_to_grammar_defn="translation/grammar/cbmc.txt", | ||
| start="cbmc_clause", | ||
| transformer=ToAst(), | ||
| ) |
Contributor
There was a problem hiding this comment.
🧹 Nitpick | 🔵 Trivial
Duplicate parser initialisation — extract to base class.
RemovePreconditions.__init__ and MovePreconditionsToAssignsAndEnsures.__init__ construct an identical Parser instance (same grammar path, same start, same transformer). Moving this to SpecificationTransformation.__init__ eliminates the duplication and ensures future subclasses get the parser for free.
♻️ Proposed refactor — consolidate in base class
In specification_transformation.py:
+from translation.ast.cbmc_ast import CBMCAst, ToAst
from translation.parser import Parser
...
class SpecificationTransformation(ABC):
+ def __init__(self) -> None:
+ self._parser = Parser(
+ path_to_grammar_defn="translation/grammar/cbmc.txt",
+ start="cbmc_clause",
+ transformer=ToAst(),
+ )
- _parser: Parser[CBMCAst]Then remove the identical __init__ bodies from both RemovePreconditions and MovePreconditionsToAssignsAndEnsures.
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@specifications/variants/transformations/remove_preconditions.py` around lines
17 - 21, Both RemovePreconditions.__init__ and
MovePreconditionsToAssignsAndEnsures.__init__ duplicate construction of the
Parser (Parser(path_to_grammar_defn="translation/grammar/cbmc.txt",
start="cbmc_clause", transformer=ToAst())); move that Parser initialization into
SpecificationTransformation.__init__ so subclasses inherit it: add self._parser
= Parser(...) to SpecificationTransformation.__init__ (using the same
path_to_grammar_defn, start and transformer symbols) and remove the identical
self._parser assignments from RemovePreconditions.__init__ and
MovePreconditionsToAssignsAndEnsures.__init__ so there’s a single source of
truth for the parser.
Comment on lines
+44
to
+71
| if not precondition_asts: | ||
| return [specification] | ||
|
|
||
| postconditions = list(specification.postconditions) | ||
| transformed_specs: list[FunctionSpecification] = [] | ||
|
|
||
| # Generate a variant for each precondition removed individually, starting from the last. | ||
| # Starting from the last is done because preconditions are generally order-dependent | ||
| # (i.e., facts assumed in a prior postcondition may be used in the next). | ||
| for i in reversed(range(len(precondition_asts))): | ||
| preconditions_to_keep = [ | ||
| ast.to_string() for j, ast in enumerate(precondition_asts) if j != i | ||
| ] | ||
| transformed_specs.append( | ||
| FunctionSpecification( | ||
| preconditions=preconditions_to_keep, | ||
| postconditions=postconditions, | ||
| ) | ||
| ) | ||
|
|
||
| # Generate a variant with all preconditions removed (if not already covered). | ||
| if len(precondition_asts) > 1: | ||
| transformed_specs.append( | ||
| FunctionSpecification( | ||
| preconditions=[], | ||
| postconditions=postconditions, | ||
| ) | ||
| ) |
Contributor
There was a problem hiding this comment.
ValueError crash when input specification has preconditions but no postconditions.
FunctionSpecification.__init__ raises ValueError when both preconditions and postconditions are empty. RemovePreconditions.apply hits this in two code paths whenever specification.postconditions is empty:
- Single precondition (line 57–62):
preconditions_to_keep = [],postconditions = []→ crash. - Multiple preconditions (line 66–71): the "all removed" variant sets
preconditions=[],postconditions=[]→ crash.
A spec with only preconditions is a valid FunctionSpecification input. MovePreconditionsToAssignsAndEnsures.apply guards against this at its line 51–52; RemovePreconditions has no equivalent guard. There is also no test covering this scenario.
🐛 Proposed fix — add early-return guard (mirrors sibling transformation)
if not precondition_asts:
return [specification]
+ # If there are no postconditions, removing all preconditions would produce an
+ # empty (invalid) spec; return unchanged.
+ if not specification.postconditions:
+ return [specification]
+
postconditions = list(specification.postconditions)🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@specifications/variants/transformations/remove_preconditions.py` around lines
44 - 71, Remove the ValueError by adding the same early-return guard used in
MovePreconditionsToAssignsAndEnsures.apply: in RemovePreconditions.apply, check
if specification.postconditions is empty and if so return [specification]
immediately; this prevents constructing FunctionSpecification with both
preconditions=[] and postconditions=[] when generating the single-removed and
all-removed variants, preserving valid inputs and avoiding the crash in
FunctionSpecification.__init__.
|
|
||
| # Generate a variant for each precondition removed individually, starting from the last. | ||
| # Starting from the last is done because preconditions are generally order-dependent | ||
| # (i.e., facts assumed in a prior postcondition may be used in the next). |
Contributor
There was a problem hiding this comment.
Comment typo: "postcondition" → "precondition".
- # (i.e., facts assumed in a prior postcondition may be used in the next).
+ # (i.e., facts assumed in a prior precondition may be used in the next).🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@specifications/variants/transformations/remove_preconditions.py` at line 52,
The inline comment in remove_preconditions.py contains a typo: replace the word
"postcondition" with "precondition" in the sentence "(i.e., facts assumed in a
prior postcondition may be used in the next)" so it reads "(i.e., facts assumed
in a prior precondition may be used in the next)"; locate the comment in the
module (around the block explaining precondition handling) and update the
wording accordingly.
Copilot stopped work on behalf of
jyoo980 due to an error
March 30, 2026 18:10
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
@CodeRabbit pause