Implementing initial spec transformer

specifications/__init__.py

@@ -1,5 +1,6 @@
 from .llm_specification_generator import LlmSpecificationGenerator
-from .specification_extractor import extract_spec_from_response
 from .simplify_spec import simplify
+from .specification_extractor import extract_spec_from_response
+from .variants.specification_variant_factory import SpecificationVariantFactory
 
-__all__ = ["LlmSpecificationGenerator", "extract_spec_from_response", "simplify"]
+__all__ = ["LlmSpecificationGenerator", "extract_spec_from_response", "simplify", "SpecificationVariantFactory"]

specifications/variants/__init__.py

@@ -0,0 +1,3 @@
+from .specification_variant_factory import SpecificationVariantFactory
+
+__all__ = ["SpecificationVariantFactory"]

specifications/variants/specification_variant_factory.py

@@ -0,0 +1,44 @@
+"""Class for symbolically generating variants of a specification."""
+
+from util import FunctionSpecification
+
+from .transformations import (
+    InferNonNullPreconditionsFromEnsures,
+    MovePreconditionsToAssignsAndEnsures,
+    RemovePreconditions,
+    SpecificationTransformation,
+)
+
+
+class SpecificationVariantFactory:
+    """Class for symbolically generating variants of a specification.
+
+    Attributes:
+        (_transformations): tuple[SpecificationTransformation, ...]: The transformations to apply
+            to a specification to generate variants.
+
+    """
+
+    _transformations: tuple[SpecificationTransformation, ...]
+
+    def __init__(self) -> None:
+        """Create a new SpecificationVariantFactory."""
+        self._transformations = (
+            MovePreconditionsToAssignsAndEnsures(),
+            RemovePreconditions(),
+            InferNonNullPreconditionsFromEnsures(),
+        )
+
+    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.
+        """
+        variants = set()
+        for transformation in self._transformations:
+            variants.update(transformation.apply(spec))
+        return tuple(variants)

specifications/variants/transformations/__init__.py

@@ -0,0 +1,7 @@
+from .specification_transformation import SpecificationTransformation
+from .move_preconditions_to_assigns_and_ensures import MovePreconditionsToAssignsAndEnsures
+from .remove_preconditions import RemovePreconditions
+from .infer_non_null_preconditions_from_ensures import InferNonNullPreconditionsFromEnsures
+from .minimize_conditional_assigns import MinimizeConditionalAssigns
+
+__all__ = ["SpecificationTransformation", "MovePreconditionsToAssignsAndEnsures", "RemovePreconditions", "InferNonNullPreconditionsFromEnsures", "MinimizeConditionalAssigns"]

specifications/variants/transformations/infer_non_null_preconditions_from_ensures.py

@@ -0,0 +1,107 @@
+"""Transformation for inferring non-null preconditions from ensures clauses."""
+
+from lark.tree import Meta
+
+from translation.ast.cbmc_ast import (
+    CbmcAst,
+    EnsuresClause,
+    IndexOp,
+    Name,
+    NeqOp,
+    PtrMemberOp,
+    RequiresClause,
+)
+from util import FunctionSpecification
+
+from .specification_transformation import SpecificationTransformation
+
+
+class InferNonNullPreconditionsFromEnsures(SpecificationTransformation):
+    """Transformation for inferring non-null preconditions from ensures clauses."""
+
+    def apply(self, specification: FunctionSpecification) -> list[FunctionSpecification]:
+        """Return the result of applying this transformation to the given specification.
+
+        Infer non-null preconditions from an ensures clause.
+
+        For example, given a spec with the following ensures clause:
+
+                    __CPROVER_ensures(a->b->c != NULL)
+
+        The following preconditions are generated:
+
+                    __CPROVER_requires(a != NULL)
+                    __CPROVER_requires(a->b != NULL)
+
+        Args:
+            specification (FunctionSpecification): The specification to transform.
+
+        Returns:
+            list[FunctionSpecification]: The result of applying this transformation to the given
+                specification.
+        """
+        precondition_asts, postcondition_asts = self._parse_specification(specification)
+        non_null_check_exprs: list[NeqOp] = [
+            non_null_check_expr
+            for ast in postcondition_asts
+            if (non_null_check_expr := self._get_non_null_check_expr(ast))
+        ]
+        precondition_exprs = []
+        for neqop in non_null_check_exprs:
+            non_null_check_subexprs = self._get_non_null_check_subexpressions(neqop.left)
+            precondition_exprs = [
+                NeqOp(subexpr, neqop.right) for subexpr in non_null_check_subexprs
+            ]
+        new_precondition_clauses = [
+            # The `Meta` here shouldn't matter, since it isn't used when inserting specs.
+            RequiresClause(meta=Meta(), expr=expr)
+            for expr in precondition_exprs
+        ]
+        updated_precondition_clauses = precondition_asts + new_precondition_clauses
+        return [
+            FunctionSpecification(
+                preconditions=[clause.to_string() for clause in updated_precondition_clauses],
+                postconditions=specification.postconditions,
+            )
+        ]
+
+    def _get_non_null_check_expr(self, ast: CbmcAst) -> NeqOp | None:
+        """Return a non-null check expression in an ensures clause, if found.
+
+        Args:
+            ast (CbmcAst): The AST in which to search for a non-null check expression.
+
+        Returns:
+            NeqOp | None: The non-null check expression, if found.
+        """
+        if not isinstance(ast, EnsuresClause):
+            return None
+        match ast.expr:
+            case NeqOp(left=PtrMemberOp(_, _), right=Name("NULL")):
+                return ast.expr
+            case NeqOp(left=IndexOp(value=PtrMemberOp(_, _)), right=Name("NULL")):
+                return ast.expr
+            case _:
+                return None
+
+    def _get_non_null_check_subexpressions(self, expr: CbmcAst) -> list[CbmcAst]:
+        """Return the subexpressions from the left-hand side of a non-null check.
+
+        Note: This function assumes the non-null check is of the form `LHS != NULL`.
+
+        Args:
+            expr (CbmcAst): The left-hand side of a non-null check.
+
+        Returns:
+            list[CbmcAst]: The subexpressions from the left-hand side of a non-null check.
+        """
+        result = []
+        match expr:
+            case PtrMemberOp(_, _):
+                subexprs = expr.get_dereference_subexpressions()
+                # Exclude self to avoid duplicating the existing ensures clause.
+                result = [s for s in subexprs if s is not expr]
+            case IndexOp(value=PtrMemberOp(_, _), index=_):
+                subexprs = expr.value.get_dereference_subexpressions()
+                result = [s for s in subexprs if s is not expr.value]
+        return result

specifications/variants/transformations/minimize_conditional_assigns.py

@@ -0,0 +1,96 @@
+"""Transformation where the condition in an assigns clause is minimized."""
+
+from translation.ast.cbmc_ast import Assigns, CbmcAst, LogicalBinOp
+from util import FunctionSpecification
+
+from .specification_transformation import SpecificationTransformation
+
+
+class MinimizeConditionalAssigns(SpecificationTransformation):
+    """Transformation where the condition in an assigns clause is minimized."""
+
+    def apply(self, specification: FunctionSpecification) -> list[FunctionSpecification]:
+        """Return the result of applying this transformation to the given specification.
+
+        Given a specification that has a postcondition such as:
+
+                __CPROVER_assigns(a || b || c : result)
+
+        Return specifications that are identical to the original, but with disjuncts removed
+        one-by-one, i.e.,
+
+                __CPROVER_assigns(a || b : result)
+                __CPROVER_assigns(a : result)
+                __CPROVER_assigns(result)
+
+        Args:
+            specification (FunctionSpecification): The specification to transform.
+
+        Returns:
+            list[FunctionSpecification]: The result of applying this transformation to the given
+                specification.
+        """
+        _, postconditions = self._parse_specification(specification)
+        assigns_clauses = [clause for clause in postconditions if isinstance(clause, Assigns)]
+
+        if not assigns_clauses:
+            return [specification]
+
+        assigns_clause = assigns_clauses[0]
+
+        # If there is no condition, nothing to minimize.
+        if assigns_clause.condition is None:
+            return [specification]
+
+        preconditions = list(specification.preconditions)
+        transformed_specs: list[FunctionSpecification] = []
+
+        # Build the non-assigns postconditions (unchanged across variants).
+        other_postconditions = [
+            clause.to_string() for clause in postconditions if not isinstance(clause, Assigns)
+        ]
+
+        # If the condition is a LogicalBinOp, generate prefix variants.
+        if isinstance(assigns_clause.condition, LogicalBinOp):
+            prefixes = assigns_clause.condition.get_operand_prefixes()
+            for prefix_condition in reversed(prefixes):
+                new_assigns = Assigns(condition=prefix_condition, targets=assigns_clause.targets)
+                new_postconditions = [*other_postconditions, new_assigns.to_string()]
+                transformed_specs.append(
+                    FunctionSpecification(
+                        preconditions=preconditions,
+                        postconditions=new_postconditions,
+                    )
+                )
+
+        # Always add a variant with no condition at all (just the assigns target).
+        no_condition_assigns = Assigns(condition=None, targets=assigns_clause.targets)
+        no_condition_postconditions = [*other_postconditions, no_condition_assigns.to_string()]
+        transformed_specs.append(
+            FunctionSpecification(
+                preconditions=preconditions,
+                postconditions=no_condition_postconditions,
+            )
+        )
+
+        return transformed_specs
+
+    def _get_operand_prefixes(self, logical_binop: LogicalBinOp) -> list[CbmcAst]:
+        """Return the strict prefixes of the given logical binary operation.
+
+        E.g., Given `a || b || c || d`, return `a`, `a || b`, `a || b || c`.
+
+        Args:
+            logical_binop (LogicalBinOp): The logical binary operation for which to return prefixes.
+
+        Returns:
+            list[CbmcAst]: The strict prefixes of the logical binary operation.
+        """
+        operands = logical_binop.get_operand_atoms()
+        if len(operands) <= 1:
+            return []
+        variants: list[CbmcAst] = []
+        for i in range(1, len(operands)):
+            prefix = operands[:i]
+            variants.append(logical_binop.apply(prefix))
+        return variants

specifications/variants/transformations/move_preconditions_to_assigns_and_ensures.py

@@ -0,0 +1,82 @@
+"""Transformation where expressions in preconditions are moved to assigns and ensures clauses."""
+
+from translation.ast.cbmc_ast import (
+    AndOp,
+    Assigns,
+    CbmcAst,
+    EnsuresClause,
+    OrOp,
+    RequiresClause,
+)
+from util import FunctionSpecification
+
+from .specification_transformation import SpecificationTransformation
+
+
+class MovePreconditionsToAssignsAndEnsures(SpecificationTransformation):
+    """Transformation where precondition expressions are moved to assigns and ensures clauses.
+
+    There are cases where a specification might contain preconditions that are *too* strong,
+    effectively weakening the entire specification. This transformation moves precondition
+    expressions into conditions for assigns clauses and disjunctions for ensures clauses.
+    """
+
+    def apply(self, specification: FunctionSpecification) -> list[FunctionSpecification]:
+        """Return the result of applying this transformation to the given specification.
+
+        Move the expressions in preconditions clauses into:
+            * Conditions for any assigns clauses.
+            * Disjunctions with any ensures clauses.
+
+        Args:
+            specification (FunctionSpecification): The specification to transform.
+
+        Returns:
+            list[FunctionSpecification]: The result of applying this transformation to the given
+                specification.
+        """
+        precondition_asts, postcondition_asts = self._parse_specification(specification)
+
+        # If there are no postconditions, return unchanged.
+        if not postcondition_asts:
+            return [specification]
+
+        # Extract the inner expressions from each RequiresClause.
+        precondition_exprs: list[CbmcAst] = [
+            clause.expr for clause in precondition_asts if isinstance(clause, RequiresClause)
+        ]
+
+        # If there are no precondition expressions, return unchanged.
+        if not precondition_exprs:
+            return [specification]
+
+        new_postconditions: list[str] = []
+        for post_ast in postcondition_asts:
+            if isinstance(post_ast, EnsuresClause):
+                # Build disjunction: !pre1 || !pre2 || ... || ensures_expr
+                result: CbmcAst = precondition_exprs[0].negate()
+                for pre_expr in precondition_exprs[1:]:
+                    result = OrOp(left=result, right=pre_expr.negate())
+                result = OrOp(left=result, right=post_ast.expr)
+                new_postconditions.append(
+                    EnsuresClause(meta=post_ast.meta, expr=result).to_string()
+                )
+            elif isinstance(post_ast, Assigns):
+                # Add conjunction of all precondition expressions as a condition.
+                condition: CbmcAst = precondition_exprs[0]
+                for pre_expr in precondition_exprs[1:]:
+                    condition = AndOp(left=condition, right=pre_expr)
+                # If there's already a condition, AND it with the preconditions.
+                if post_ast.condition:
+                    condition = AndOp(left=post_ast.condition, right=condition)
+                new_assigns = Assigns(condition=condition, targets=post_ast.targets)
+                new_postconditions.append(new_assigns.to_string())
+            else:
+                new_postconditions.append(post_ast.to_string())
+
+        return [
+            FunctionSpecification(
+                preconditions=[],
+                postconditions=new_postconditions,
+            )
+        ]