diff --git a/specifications/__init__.py b/specifications/__init__.py index db9590e3..74fc1382 100644 --- a/specifications/__init__.py +++ b/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"] \ No newline at end of file +__all__ = ["LlmSpecificationGenerator", "extract_spec_from_response", "simplify", "SpecificationVariantFactory"] \ No newline at end of file diff --git a/specifications/variants/__init__.py b/specifications/variants/__init__.py new file mode 100644 index 00000000..3fc4b844 --- /dev/null +++ b/specifications/variants/__init__.py @@ -0,0 +1,3 @@ +from .specification_variant_factory import SpecificationVariantFactory + +__all__ = ["SpecificationVariantFactory"] \ No newline at end of file diff --git a/specifications/variants/specification_variant_factory.py b/specifications/variants/specification_variant_factory.py new file mode 100644 index 00000000..084a254b --- /dev/null +++ b/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) diff --git a/specifications/variants/transformations/__init__.py b/specifications/variants/transformations/__init__.py new file mode 100644 index 00000000..822e7f2a --- /dev/null +++ b/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"] \ No newline at end of file diff --git a/specifications/variants/transformations/infer_non_null_preconditions_from_ensures.py b/specifications/variants/transformations/infer_non_null_preconditions_from_ensures.py new file mode 100644 index 00000000..a7abdf79 --- /dev/null +++ b/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 diff --git a/specifications/variants/transformations/minimize_conditional_assigns.py b/specifications/variants/transformations/minimize_conditional_assigns.py new file mode 100644 index 00000000..300b04b1 --- /dev/null +++ b/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 diff --git a/specifications/variants/transformations/move_preconditions_to_assigns_and_ensures.py b/specifications/variants/transformations/move_preconditions_to_assigns_and_ensures.py new file mode 100644 index 00000000..524ffc93 --- /dev/null +++ b/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, + ) + ] diff --git a/specifications/variants/transformations/remove_preconditions.py b/specifications/variants/transformations/remove_preconditions.py new file mode 100644 index 00000000..958290e2 --- /dev/null +++ b/specifications/variants/transformations/remove_preconditions.py @@ -0,0 +1,61 @@ +"""Transformation where preconditions are removed, one-by-one.""" + +from util import FunctionSpecification + +from .specification_transformation import SpecificationTransformation + + +class RemovePreconditions(SpecificationTransformation): + """Transformation where precondition expressions are removed one-by-one.""" + + def apply(self, specification: FunctionSpecification) -> list[FunctionSpecification]: + """Return the result of applying this transformation to the given specification. + + Remove the precondition(s) of this specification, one-by-one. + + For example, given a spec with preconditions [p0, p1], this function returns specs + that have preconditions: + * [p0] (p1 removed) + * [p1] (p0 removed) + * [] (all removed) + While leaving the postconditions unchanged. + + Args: + specification (FunctionSpecification): The specification to transform. + + Returns: + list[FunctionSpecification]: The result of applying this transformation to the given + specification. + """ + precondition_asts, _ = self._parse_specification(specification) + + 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, + ) + ) + + return transformed_specs diff --git a/specifications/variants/transformations/specification_transformation.py b/specifications/variants/transformations/specification_transformation.py new file mode 100644 index 00000000..6870b010 --- /dev/null +++ b/specifications/variants/transformations/specification_transformation.py @@ -0,0 +1,56 @@ +"""Represent a transformation of a specification.""" + +from abc import ABC, abstractmethod + +from translation.ast.cbmc_ast import CbmcAst, ToAst +from translation.parser import Parser +from util import FunctionSpecification + + +class SpecificationTransformation(ABC): + """Represent a transformation of a specification. + + Attributes: + parser (Parser[CbmcAst]): A parser for CBMC ASTs. + """ + + _parser: Parser[CbmcAst] + + def __init__(self): + """Create a new SpecificationTransformation.""" + self.parser = Parser( + path_to_grammar_defn="translation/grammar/cbmc.txt", + start="cbmc_clause", + transformer=ToAst(), + ) + + @abstractmethod + def apply(self, specification: FunctionSpecification) -> list[FunctionSpecification]: + """Return the result(s) of applying this transformation to the given specification. + + Args: + specification (FunctionSpecification): The specification to which to apply this + transformation + + Returns: + list[FunctionSpecification]: The result(s) of applying this specification to the given + specification. + """ + ... + + def _parse_specification( + self, specification: FunctionSpecification + ) -> tuple[list[CbmcAst], list[CbmcAst]]: + """Return the given specification's pre and postcondition(s) as CBMC ASTs. + + Args: + specification (FunctionSpecification): The specification to parse. + + Returns: + tuple[list[CbmcAst], list[CbmcAst]]: The parsed pre and postcondition(s) of the given + specification. + """ + return ( + [self.parser.parse(clause) for clause in specification.preconditions], + [self.parser.parse(clause) for clause in specification.postconditions], + ) diff --git a/test/specifications/__init__.py b/test/specifications/__init__.py new file mode 100644 index 00000000..e69de29b diff --git a/test/specifications/transformations/__init__.py b/test/specifications/transformations/__init__.py new file mode 100644 index 00000000..e69de29b diff --git a/test/specifications/transformations/test_infer_non_null_preconditions_from_ensures.py b/test/specifications/transformations/test_infer_non_null_preconditions_from_ensures.py new file mode 100644 index 00000000..004274dc --- /dev/null +++ b/test/specifications/transformations/test_infer_non_null_preconditions_from_ensures.py @@ -0,0 +1,36 @@ +from specifications.variants.transformations import InferNonNullPreconditionsFromEnsures +from util import FunctionSpecification + +transformation = InferNonNullPreconditionsFromEnsures() + + +def test_ensures_value_non_null(): + spec_with_non_null_ensures = FunctionSpecification( + preconditions=[], postconditions=["__CPROVER_ensures(foo->bar->baz->james != NULL)"] + ) + spec_with_updated_preconditions = transformation.apply(spec_with_non_null_ensures)[0] + assert spec_with_updated_preconditions.preconditions == [ + "__CPROVER_requires((foo != NULL))", + "__CPROVER_requires((foo->bar != NULL))", + "__CPROVER_requires((foo->bar->baz != NULL))", + ] + assert ( + spec_with_updated_preconditions.postconditions == spec_with_non_null_ensures.postconditions + ) + + +def test_infers_precondition_with_existing_preconditions(): + spec_with_non_null_ensures = FunctionSpecification( + preconditions=["__CPROVER_requires(z < INT_MAX)"], + postconditions=["__CPROVER_ensures(a->b->c->arr[0] != NULL)"], + ) + spec_with_updated_preconditions = transformation.apply(spec_with_non_null_ensures)[0] + assert spec_with_updated_preconditions.preconditions == [ + "__CPROVER_requires((z < INT_MAX))", + "__CPROVER_requires((a != NULL))", + "__CPROVER_requires((a->b != NULL))", + "__CPROVER_requires((a->b->c != NULL))", + ] + assert ( + spec_with_updated_preconditions.postconditions == spec_with_non_null_ensures.postconditions + ) diff --git a/test/specifications/transformations/test_minimize_conditional_assigns.py b/test/specifications/transformations/test_minimize_conditional_assigns.py new file mode 100644 index 00000000..1628599d --- /dev/null +++ b/test/specifications/transformations/test_minimize_conditional_assigns.py @@ -0,0 +1,25 @@ +from specifications.variants.transformations import MinimizeConditionalAssigns +from util import FunctionSpecification + +transformation = MinimizeConditionalAssigns() + +def test_minimize_single_condition_in_assigns() -> None: + spec_with_single_condition_in_assigns = FunctionSpecification(preconditions=[], postconditions=[ + "__CPROVER_ensures(__CPROVER_return_value > 1)", + "__CPROVER_assigns(out->target != NULL : out->target)" + ]) + transformed_specs = transformation.apply(spec_with_single_condition_in_assigns) + assert transformed_specs == [ + FunctionSpecification(preconditions=[], postconditions=[ + "__CPROVER_ensures((__CPROVER_return_value > 1))", + "__CPROVER_assigns(out->target)" + ]) + ] + +def test_minimize_multiple_condition_in_assigns() -> None: + spec_with_binop_condition_in_assigns = FunctionSpecification(preconditions=[], postconditions=[ + "__CPROVER_ensures(__CPROVER_return_value > 1)", + "__CPROVER_assigns(out->target != NULL && foo && bar : out->target)" + ]) + transformed_specs = transformation.apply(spec_with_binop_condition_in_assigns) + print(transformed_specs) \ No newline at end of file diff --git a/test/specifications/transformations/test_move_preconditions_to_assigns_and_ensures.py b/test/specifications/transformations/test_move_preconditions_to_assigns_and_ensures.py new file mode 100644 index 00000000..8d03e357 --- /dev/null +++ b/test/specifications/transformations/test_move_preconditions_to_assigns_and_ensures.py @@ -0,0 +1,56 @@ +from specifications.variants.transformations import MovePreconditionsToAssignsAndEnsures +from util import FunctionSpecification + +transformation = MovePreconditionsToAssignsAndEnsures() + + +def test_move_preconditions_to_ensures_returns_unchanged_specs_if_no_ensures_clause(): + spec_without_ensures = FunctionSpecification( + preconditions=[ + "__CPROVER_requires(pp->p != NULL)", + "__CPROVER_requires(pp->p->buf != NULL)", + ], + postconditions=[], + ) + actual_transformed_spec = transformation.apply(spec_without_ensures)[0] + assert actual_transformed_spec == spec_without_ensures + + +def test_move_preconditions_to_ensures_disjunctions(): + spec_with_preconditions = FunctionSpecification( + preconditions=[ + "__CPROVER_requires(pp != NULL)", + "__CPROVER_requires(pp->p != NULL)", + "__CPROVER_requires(pp->p->buf != NULL)", + "__CPROVER_requires(some_call(foo))", + ], + postconditions=["__CPROVER_ensures(pp->p->buf[0] == 0)"], + ) + actual_transformed_spec = transformation.apply(spec_with_preconditions)[0] + expected_transformed_spec = FunctionSpecification( + preconditions=[], + postconditions=[ + "__CPROVER_ensures((((((pp == NULL) || (pp->p == NULL)) || (pp->p->buf == NULL)) || !some_call(foo)) || (pp->p->buf[0] == 0)))" + ], + ) + assert actual_transformed_spec == expected_transformed_spec + + +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)[0] + 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 diff --git a/test/specifications/transformations/test_remove_preconditions.py b/test/specifications/transformations/test_remove_preconditions.py new file mode 100644 index 00000000..dd0bf484 --- /dev/null +++ b/test/specifications/transformations/test_remove_preconditions.py @@ -0,0 +1,39 @@ +from specifications.variants.transformations import RemovePreconditions +from util import FunctionSpecification + +transformation = RemovePreconditions() + + +def test_remove_preconditions_returns_unchanged_if_no_preconditions(): + spec_without_preconditions = FunctionSpecification( + preconditions=[ + ], + postconditions=["__CPROVER_ensures(__CPROVER_return_value > 0)"], + ) + actual_transformed_specs = transformation.apply(spec_without_preconditions) + assert actual_transformed_specs == [spec_without_preconditions] + +def test_remove_preconditions_single_precondition(): + spec_single_precondition = FunctionSpecification( + preconditions=[ + "__CPROVER_requires(a > 0)" + ], + postconditions=["__CPROVER_ensures(__CPROVER_return_value > 0)"], + ) + actual_transformed_specs = transformation.apply(spec_single_precondition) + assert actual_transformed_specs == [FunctionSpecification(preconditions=[], postconditions=["__CPROVER_ensures(__CPROVER_return_value > 0)"])] + +def test_remove_preconditions_more_than_one_precondition(): + spec_multiple_preconditions = FunctionSpecification( + preconditions=[ + "__CPROVER_requires(a > 0)", + "__CPROVER_requires(len < INT_MAX)" + ], + postconditions=["__CPROVER_ensures(__CPROVER_return_value > 0)"], + ) + actual_transformed_specs = transformation.apply(spec_multiple_preconditions) + assert actual_transformed_specs == [ + FunctionSpecification(preconditions=["__CPROVER_requires((a > 0))"], postconditions=["__CPROVER_ensures(__CPROVER_return_value > 0)"]), + FunctionSpecification(preconditions=["__CPROVER_requires((len < INT_MAX))"], postconditions=["__CPROVER_ensures(__CPROVER_return_value > 0)"]), + FunctionSpecification(preconditions=[], postconditions=["__CPROVER_ensures(__CPROVER_return_value > 0)"]) + ] \ No newline at end of file diff --git a/test/translation/test_cbmc_specification_mutant_generator.py b/test/translation/test_cbmc_specification_mutant_generator.py index 5b4e456c..210eb5e2 100644 --- a/test/translation/test_cbmc_specification_mutant_generator.py +++ b/test/translation/test_cbmc_specification_mutant_generator.py @@ -3,7 +3,6 @@ AndOp, Bool, BuiltinType, - CbmcAst, DivOp, EnsuresClause, EqOp, diff --git a/translation/ast/cbmc_ast.py b/translation/ast/cbmc_ast.py index 8fa9c5e3..921a942c 100644 --- a/translation/ast/cbmc_ast.py +++ b/translation/ast/cbmc_ast.py @@ -30,33 +30,77 @@ def get_mutation_candidates(self) -> list[type[CbmcAst]]: class CbmcAst(ast_utils.Ast, Mutable): - pass + def to_string(self) -> str: + """Convert this AST node to its string representation. + + Returns: + str: The string form of this AST node. + """ + raise NotImplementedError(f"to_string not implemented for {type(self).__name__}") + + def negate(self) -> "CbmcAst": + """Return the negation of this AST node. + + Note: This is a general case that avoids crashes at run-time (but may not be sound). + + Returns: + CbmcAst: The negation of this AST node. + """ + return NotOp(self) def is_boolean_expression(self) -> bool: return False +def _to_str(node: Any) -> str: + """Convert an AST node or primitive value to a string. + + Args: + node: A CbmcAst node or a primitive value. + + Returns: + str: The string representation. + """ + if node is None: + return "" + if isinstance(node, CbmcAst): + return node.to_string() + return str(node) + + @dataclass(frozen=True) class RequiresClause(CbmcAst, ast_utils.WithMeta): meta: Meta expr: Any + def to_string(self) -> str: + return f"__CPROVER_requires({_to_str(self.expr)})" + @dataclass(frozen=True) class EnsuresClause(CbmcAst, ast_utils.WithMeta): meta: Meta expr: Any + def to_string(self) -> str: + return f"__CPROVER_ensures({_to_str(self.expr)})" + @dataclass(frozen=True) class ExprList(CbmcAst, ast_utils.AsList): items: tuple[CbmcAst, ...] + def to_string(self) -> str: + return ", ".join(_to_str(item) for item in self.items) + @dataclass(frozen=True) class AssignsTargetList(CbmcAst): items: ExprList + def to_string(self) -> str: + return _to_str(self.items) + @dataclass(frozen=True) class Assigns(CbmcAst): @@ -65,6 +109,13 @@ class Assigns(CbmcAst): condition: Any | None targets: AssignsTargetList + def to_string(self) -> str: + targets = _to_str(self.targets) + if self.condition: + cond = _to_str(self.condition) + return f"__CPROVER_assigns({cond} : {targets})" + return f"__CPROVER_assigns({targets})" + @dataclass(frozen=True) class FreesTargetList(CbmcAst): @@ -130,16 +181,25 @@ class Freeable(CbmcAst): class Name(CbmcAst): name: str + def to_string(self) -> str: + return self.name + @dataclass(frozen=True) class Number(CbmcAst): value: Any + def to_string(self) -> str: + return str(self.value) + @dataclass(frozen=True) class Bool(CbmcAst): value: bool + def to_string(self) -> str: + return "1" if self.value else "0" + def is_boolean_expression(self) -> bool: return True @@ -148,16 +208,68 @@ def is_boolean_expression(self) -> bool: class StringLit(CbmcAst): value: str + def to_string(self) -> str: + return self.value + -@dataclass(frozen=True) class BinOp(ABC, CbmcAst): left: Any right: Any + __match_args__ = ("left", "right") + @abstractmethod def operator(self) -> str: raise NotImplementedError("Subclasses must implement this method") + def to_string(self) -> str: + return f"({_to_str(self.left)} {self.operator()} {_to_str(self.right)})" + + +class LogicalBinOp(BinOp): + def __init__(self, left: Any, right: Any): + self.left = left + self.right = right + + def get_operand_atoms(self) -> list[CbmcAst]: + match self: + case LogicalBinOp(left=LogicalBinOp(_, _), right=LogicalBinOp(_, _)): + return self.left.get_operand_atoms() + self.right.get_operand_atoms() + case LogicalBinOp(left=LogicalBinOp(_, _), right=rhs): + return self.left.get_operand_atoms() + [rhs] + case LogicalBinOp(left=lhs, right=LogicalBinOp(_, _)): + return [lhs] + self.right.get_operand_atoms() + case _: + return [self.left, self.right] + + def get_operand_prefixes(self) -> list[CbmcAst]: + """Return the strict prefixes of this 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 = self.get_operand_atoms() + if len(operands) <= 1: + return [] + variants: list[CbmcAst] = [] + for i in range(1, len(operands)): + prefix = operands[:i] + variants.append(self.apply(prefix)) + return variants + + def apply(self, operands: list[CbmcAst]) -> "LogicalBinOp | CbmcAst": + if len(operands) == 1: + return operands[0] + result = operands[0] + for operand in operands[1:]: + result = type(self)(left=result, right=operand) + return result + @dataclass(frozen=True) class OrOp(BinOp): @@ -167,12 +279,12 @@ class OrOp(BinOp): def operator(self) -> str: return "||" + def negate(self) -> CbmcAst: + return AndOp(left=self.left.negate(), right=self.right.negate()) + def get_mutation_candidates(self) -> list[type[CbmcAst]]: return [AndOp] - def is_boolean_expression(self) -> bool: - return True - @dataclass(frozen=True) class AndOp(BinOp): @@ -182,6 +294,9 @@ class AndOp(BinOp): def operator(self) -> str: return "&&" + def negate(self) -> CbmcAst: + return OrOp(left=self.left.negate(), right=self.right.negate()) + def get_mutation_candidates(self) -> list[type[CbmcAst]]: return [OrOp] @@ -197,6 +312,9 @@ class EqOp(BinOp): def operator(self) -> str: return "==" + def negate(self) -> CbmcAst: + return NeqOp(left=self.left, right=self.right) + def get_mutation_candidates(self) -> list[type[CbmcAst]]: return [NeqOp] @@ -212,6 +330,9 @@ class NeqOp(BinOp): def operator(self) -> str: return "!=" + def negate(self) -> CbmcAst: + return EqOp(left=self.left, right=self.right) + def get_mutation_candidates(self) -> list[type[CbmcAst]]: return [EqOp] @@ -227,6 +348,9 @@ class LtOp(BinOp): def operator(self) -> str: return "<" + def negate(self) -> CbmcAst: + return GeOp(left=self.left, right=self.right) + def get_mutation_candidates(self) -> list[type[CbmcAst]]: return [GeOp] @@ -242,6 +366,9 @@ class LeOp(BinOp): def operator(self) -> str: return "<=" + def negate(self) -> CbmcAst: + return GtOp(left=self.left, right=self.right) + def get_mutation_candidates(self) -> list[type[CbmcAst]]: return [GtOp] @@ -257,6 +384,9 @@ class GtOp(BinOp): def operator(self) -> str: return ">" + def negate(self) -> CbmcAst: + return LeOp(left=self.left, right=self.right) + def get_mutation_candidates(self) -> list[type[CbmcAst]]: return [LeOp] @@ -272,6 +402,9 @@ class GeOp(BinOp): def operator(self) -> str: return ">=" + def negate(self) -> CbmcAst: + return LtOp(left=self.left, right=self.right) + def get_mutation_candidates(self) -> list[type[CbmcAst]]: return [LtOp] @@ -344,55 +477,103 @@ def get_mutation_candidates(self) -> list[type[CbmcAst]]: class NotOp(CbmcAst): operand: Any + def to_string(self) -> str: + return f"!{_to_str(self.operand)}" + + def negate(self) -> CbmcAst: + return self.operand + @dataclass(frozen=True) class AddrOp(CbmcAst): operand: Any + def to_string(self) -> str: + return f"&{_to_str(self.operand)}" + @dataclass(frozen=True) class DerefOp(CbmcAst): operand: Any + def to_string(self) -> str: + return f"*{_to_str(self.operand)}" + @dataclass(frozen=True) class NegOp(CbmcAst): operand: Any + def to_string(self) -> str: + return f"-({_to_str(self.operand)})" + @dataclass(frozen=True) class PosOp(CbmcAst): operand: Any + def to_string(self) -> str: + return f"+({_to_str(self.operand)})" + @dataclass(frozen=True) class MemberOp(CbmcAst): value: CbmcAst attr: CbmcAst + def to_string(self) -> str: + attr = self.attr.name if isinstance(self.attr, Name) else _to_str(self.attr) + return f"{_to_str(self.value)}.{attr}" + @dataclass(frozen=True) 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}" + + def get_dereference_subexpressions(self) -> list["PtrMemberOp | CbmcAst"]: + """Return the chain of subexpressions that are dereferenced in this pointer member access. + + E.g., Given `foo->bar->baz`, return [`foo`, `foo->bar`, `foo->bar->baz`], since each + is a pointer that must be non-null for the full expression to be valid. + + Returns: + list[CbmcAst]: The subexpressions that are dereferenced in this chain, including self. + """ + if isinstance(self.value, PtrMemberOp): + return self.value.get_dereference_subexpressions() + [self] + return [self.value, self] + @dataclass(frozen=True) class IndexOp(CbmcAst): value: Any index: Any + def to_string(self) -> str: + return f"{_to_str(self.value)}[{_to_str(self.index)}]" + @dataclass(frozen=True) class CallOp(CbmcAst): func: CbmcAst args: CbmcAst + def to_string(self) -> str: + return f"{_to_str(self.func)}({_to_str(self.args)})" + @dataclass(frozen=True) class ArgList(CbmcAst, ast_utils.AsList): items: tuple[Any, ...] + def to_string(self) -> str: + return ", ".join(_to_str(item) for item in self.items) + class TypeNode(CbmcAst): pass @@ -404,18 +585,27 @@ class BuiltinType(TypeNode): BUILT_IN_TYPES = {"int", "unsigned", "signed", "char", "long", "float", "double"} name: str + def to_string(self) -> str: + return self.name + @dataclass(frozen=True) class NamedType(TypeNode): # typedef or user-defined type name: Name + def to_string(self) -> str: + return _to_str(self.name) + @dataclass(frozen=True) class QuantifierDecl(CbmcAst): typenode: TypeNode name: Name + def to_string(self) -> str: + return f"{_to_str(self.typenode)} {_to_str(self.name)}" + @dataclass(frozen=True) class Quantifier(CbmcAst): @@ -429,6 +619,12 @@ class Quantifier(CbmcAst): class ForallExpr(Quantifier): kind: str = "forall" + def to_string(self) -> str: + return ( + f"__CPROVER_forall {{ {_to_str(self.decl)}; " + f"({_to_str(self.range_expr)}) ==> {_to_str(self.expr)} }}" + ) + def get_mutation_candidates(self) -> list[type[CbmcAst]]: return [ExistsExpr] @@ -437,6 +633,12 @@ def get_mutation_candidates(self) -> list[type[CbmcAst]]: class ExistsExpr(Quantifier): kind: str = "exists" + def to_string(self) -> str: + return ( + f"__CPROVER_exists {{ {_to_str(self.decl)}; " + f"({_to_str(self.range_expr)}) && {_to_str(self.expr)} }}" + ) + def get_mutation_candidates(self) -> list[type[CbmcAst]]: return [ForallExpr] @@ -445,10 +647,14 @@ def get_mutation_candidates(self) -> list[type[CbmcAst]]: class Old(CbmcAst): expr: Any + def to_string(self) -> str: + return f"__CPROVER_old({_to_str(self.expr)})" + @dataclass(frozen=True) class ReturnValue(CbmcAst): - pass + def to_string(self) -> str: + return "__CPROVER_return_value" class _ToAst(Transformer): diff --git a/translation/ast/cbmc_specification_mutant_generator.py b/translation/ast/cbmc_specification_mutant_generator.py index 7aba5a8c..9d9cd5e9 100644 --- a/translation/ast/cbmc_specification_mutant_generator.py +++ b/translation/ast/cbmc_specification_mutant_generator.py @@ -2,7 +2,8 @@ from __future__ import annotations -from typing import cast +from collections.abc import Callable +from typing import TypeAlias, cast from loguru import logger @@ -16,6 +17,8 @@ RequiresClause, ) +BinOpFactory: TypeAlias = Callable[[CbmcAst, CbmcAst], BinOp] + class CbmcSpecificationMutantGenerator: """Class to create mutants of CBMC AST nodes.""" @@ -51,11 +54,8 @@ def get_mutants(self, node: CbmcAst) -> set[CbmcAst]: case EnsuresClause(meta, expr): mutants.update({EnsuresClause(meta, m) for m in self.get_mutants(expr)}) case BinOp(left, right): - replacement_operators: list[type[BinOp]] = cast( - "list[type[BinOp]]", node.get_mutation_candidates() - ) - # Mutate just the operator, keeping children unchanged. - mutants.update({mutation(left, right) for mutation in replacement_operators}) + replacement_operators = cast("list[BinOpFactory]", node.get_mutation_candidates()) + mutants.update({make_binop(left, right) for make_binop in replacement_operators}) # Mutate just the left-hand side, keeping operator and right child. mutants.update( @@ -122,9 +122,7 @@ def get_higher_order_mutant(self, node: CbmcAst) -> CbmcAst: return EnsuresClause(meta=meta, expr=self.get_higher_order_mutant(expr)) case BinOp(left, right): # There is only one mutation candidate, for now. - replacement_operators: list[type[BinOp]] = cast( - "list[type[BinOp]]", node.get_mutation_candidates() - ) + replacement_operators = cast("list[BinOpFactory]", node.get_mutation_candidates()) assert len(replacement_operators) >= 1, ( f"Expected at least one mutation candidate for a binary operation: {node}" )