From 86f90bdbda6bf0ae724592b049e05c65c89b0240 Mon Sep 17 00:00:00 2001 From: James Yoo Date: Sat, 14 Feb 2026 07:15:17 -0800 Subject: [PATCH 01/18] Implementing initial spec transformer --- test/util/test_spec_transformer.py | 23 ++++++ translation/ast/cbmc_ast.py | 119 +++++++++++++++++++++++++++- util/spec_transformer.py | 120 +++++++++++++++++++++++++++++ 3 files changed, 258 insertions(+), 4 deletions(-) create mode 100644 test/util/test_spec_transformer.py create mode 100644 util/spec_transformer.py diff --git a/test/util/test_spec_transformer.py b/test/util/test_spec_transformer.py new file mode 100644 index 00000000..4c1f97c9 --- /dev/null +++ b/test/util/test_spec_transformer.py @@ -0,0 +1,23 @@ +from util.spec_transformer import SpecTransformer +from util import FunctionSpecification + +transformer = SpecTransformer() + + +def test_move_preconditions_to_assigns_conditional(): + spec_with_preconditions = FunctionSpecification( + preconditions=[ + "__CPROVER_requires(pp != NULL)", + "__CPROVER_requires(pp->p != NULL)", + "__CPROVER_requires(pp->p->buf != NULL)", + ], + postconditions=["__CPROVER_assigns(pp->p->buf[0])"], + ) + expected_transformed_spec = FunctionSpecification( + preconditions=[], + postconditions=[ + "__CPROVER_assigns(((pp != NULL) && ((pp->p->buf != NULL) && (pp->p != NULL))) : pp->p->buf[0])" + ], + ) + actual_transformed_spec = transformer.move_preconditions_to_assigns(spec_with_preconditions) + assert expected_transformed_spec == actual_transformed_spec diff --git a/translation/ast/cbmc_ast.py b/translation/ast/cbmc_ast.py index efd2c687..3d627142 100644 --- a/translation/ast/cbmc_ast.py +++ b/translation/ast/cbmc_ast.py @@ -17,7 +17,29 @@ class CBMCAst(ast_utils.Ast): - 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 _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 @@ -25,22 +47,34 @@ class RequiresClause(CBMCAst, ast_utils.WithMeta): meta: Meta expr: Any + def to_string(self) -> str: + return f"__CPROVER_requires({_to_str(self.expr)})" + @dataclass class EnsuresClause(CBMCAst, ast_utils.WithMeta): meta: Meta expr: Any + def to_string(self) -> str: + return f"__CPROVER_ensures({_to_str(self.expr)})" + @dataclass class ExprList(CBMCAst, ast_utils.AsList): items: list[CBMCAst] + def to_string(self) -> str: + return ", ".join(_to_str(item) for item in self.items) + @dataclass class AssignsTargetList(CBMCAst): items: ExprList + def to_string(self) -> str: + return _to_str(self.items) + @dataclass class Assigns(CBMCAst): @@ -49,26 +83,45 @@ 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 class Name(CBMCAst): name: str + def to_string(self) -> str: + return self.name + @dataclass class Number(CBMCAst): value: Any + def to_string(self) -> str: + return str(self.value) + @dataclass class Bool(CBMCAst): value: bool + def to_string(self) -> str: + return "1" if self.value else "0" + @dataclass class StringLit(CBMCAst): value: str + def to_string(self) -> str: + return self.value + @dataclass class BinOp(ABC, CBMCAst): @@ -79,6 +132,9 @@ class BinOp(ABC, CBMCAst): 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)})" + @dataclass class OrOp(BinOp): @@ -201,55 +257,87 @@ def operator(self) -> str: class NotOp(CBMCAst): operand: Any + def to_string(self) -> str: + return f"!{_to_str(self.operand)}" + @dataclass class AddrOp(CBMCAst): operand: Any + def to_string(self) -> str: + return f"&{_to_str(self.operand)}" + @dataclass class DerefOp(CBMCAst): operand: Any + def to_string(self) -> str: + return f"*{_to_str(self.operand)}" + @dataclass class NegOp(CBMCAst): operand: Any + def to_string(self) -> str: + return f"-({_to_str(self.operand)})" + @dataclass class PosOp(CBMCAst): operand: Any + def to_string(self) -> str: + return f"+({_to_str(self.operand)})" + @dataclass 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 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}" + @dataclass class IndexOp(CBMCAst): value: Any index: Any + def to_string(self) -> str: + return f"{_to_str(self.value)}[{_to_str(self.index)}]" + @dataclass class CallOp(CBMCAst): func: CBMCAst args: CBMCAst + def to_string(self) -> str: + return f"{_to_str(self.func)}({_to_str(self.args)})" + @dataclass class ArgList(CBMCAst, ast_utils.AsList): items: list[Any] + def to_string(self) -> str: + return ", ".join(_to_str(item) for item in self.items) + class TypeNode(CBMCAst): pass @@ -261,18 +349,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 class NamedType(TypeNode): # typedef or user-defined type name: Name + def to_string(self) -> str: + return _to_str(self.name) + @dataclass class QuantifierDecl(CBMCAst): typenode: TypeNode name: Name + def to_string(self) -> str: + return f"{_to_str(self.typenode)} {_to_str(self.name)}" + @dataclass class Quantifier(CBMCAst): @@ -285,23 +382,37 @@ class Quantifier(CBMCAst): @dataclass class ForallExpr(Quantifier): kind: str = "forall" - pass + + def to_string(self) -> str: + return ( + f"__CPROVER_forall {{ {_to_str(self.decl)}; " + f"({_to_str(self.range_expr)}) ==> {_to_str(self.expr)} }}" + ) @dataclass class ExistsExpr(Quantifier): kind: str = "exists" - pass + + def to_string(self) -> str: + return ( + f"__CPROVER_exists {{ {_to_str(self.decl)}; " + f"({_to_str(self.range_expr)}) && {_to_str(self.expr)} }}" + ) @dataclass class Old(CBMCAst): expr: Any + def to_string(self) -> str: + return f"__CPROVER_old({_to_str(self.expr)})" + @dataclass class ReturnValue(CBMCAst): - pass + def to_string(self) -> str: + return "__CPROVER_return_value" class _ToAst(Transformer): diff --git a/util/spec_transformer.py b/util/spec_transformer.py new file mode 100644 index 00000000..0b886503 --- /dev/null +++ b/util/spec_transformer.py @@ -0,0 +1,120 @@ +"""Class for applying transformations to specifications.""" + +from translation.ast.cbmc_ast import AndOp, Assigns, CBMCAst, RequiresClause, ToAst +from translation.parser import Parser +from util import FunctionSpecification + + +class SpecTransformer: + """Class for applying transformations to specifications. + + Attributes: + (_parser): Parser[CBMCAst]: A parser for CBMC specifications. + + """ + + _parser: Parser[CBMCAst] = Parser( + path_to_grammar_defn="translation/grammar/cbmc.txt", + start="cbmc_clause", + transformer=ToAst(), + ) + + def move_preconditions_to_assigns(self, spec: FunctionSpecification) -> FunctionSpecification: + """Return a spec where precondition expressions are moved to conditions for assigns clauses. + + There are cases where a specification might contain preconditions that are *too* strong, + effectively weakening the entire specification. Below is one example: + + ```c + void f1(struct pair_of_pairs *pp) + __CPROVER_requires(pp != NULL) + __CPROVER_requires(pp->p != NULL) + __CPROVER_requires(pp->p->buf != NULL) + __CPROVER_ensures(pp->p->buf[0] == 0) + __CPROVER_assigns(pp->p->buf[0]) + { + if(pp && pp->p && pp->p->buf) + pp->p->buf[0] = 0; + } + ``` + + It is the case that `f1` might be called with a NULL `pp` (or `pp->p` or `pp->p->buf`), and + the function accounts for this with a conditional check. A more expressive and accurate + specification would be: + + __CPROVER_ensures(pp->p->buf[0] == 0) + __CPROVER_assigns( + pp != NULL && pp->p != NULL && pp->p->buf != NULL : pp->p->buf[0] + ) + + Where each expression in a precondition is provided as a condition for the assignment + `pp->p->buf[0]`. + + Args: + spec (FunctionSpecification): The specification. + + Returns: + FunctionSpecification: The specification, where each precondition expression is moved + to a condition for assignment clauses. + """ + if not spec.preconditions: + return spec + + preconditions = [self._parser.parse(clause) for clause in spec.preconditions] + + postconditions = [self._parser.parse(clause) for clause in spec.postconditions] + precondition_exprs = [ + clause.expr for clause in preconditions if isinstance(clause, RequiresClause) + ] + conjunction_of_preconditions_exprs = self._make_conjunction_from(precondition_exprs) + + updated_postconditions = [] + for clause in postconditions: + if isinstance(clause, Assigns): + clause.condition = conjunction_of_preconditions_exprs + updated_postconditions.append(clause.to_string()) + + return FunctionSpecification(preconditions=[], postconditions=updated_postconditions) + + def move_preconditions_to_ensures(self, spec: FunctionSpecification) -> FunctionSpecification: + """TODO: Implement me. + + Args: + spec (FunctionSpecification): _description_ + + Raises: + NotImplementedError: _description_ + + Returns: + FunctionSpecification: _description_ + """ + raise NotImplementedError("TODO") + + def _get_assigns_clauses(self, spec: FunctionSpecification) -> list[Assigns]: + """Return the Assigns clauses in a specification. + + Args: + spec (FunctionSpecification): The specification. + + Returns: + list[Assigns]: The Assigns clauses in a specification. + """ + parsed_postconditions = [self._parser.parse(clause) for clause in spec.postconditions] + return [clause for clause in parsed_postconditions if isinstance(clause, Assigns)] + + def _make_conjunction_from(self, exprs: list[CBMCAst]) -> CBMCAst: + """Return a conjunction (i.e., an AndOp) comprising the given expressions. + + Args: + exprs (list[CBMCAst]): The expressions to construct a conjunction from. + + Returns: + CBMCAst: The conjunction. + """ + if len(exprs) == 1: + return exprs[0] + conjunction = AndOp(left=exprs.pop(), right=exprs.pop()) + andop = conjunction + while exprs: + andop = AndOp(left=exprs.pop(), right=andop) + return andop From c3249c885e96be59b2f56a550434cd852ad3e694 Mon Sep 17 00:00:00 2001 From: James Yoo Date: Sat, 14 Feb 2026 15:37:39 -0800 Subject: [PATCH 02/18] Avoid removing preconditions when no `Assigns` clause is present --- test/util/test_spec_transformer.py | 8 ++++++++ util/spec_transformer.py | 9 +++++++-- 2 files changed, 15 insertions(+), 2 deletions(-) diff --git a/test/util/test_spec_transformer.py b/test/util/test_spec_transformer.py index 4c1f97c9..562327c1 100644 --- a/test/util/test_spec_transformer.py +++ b/test/util/test_spec_transformer.py @@ -4,6 +4,14 @@ transformer = SpecTransformer() +def test_move_preconditions_returns_unchanged_spec_if_no_assigns(): + spec_with_no_assigns = FunctionSpecification( + preconditions=["__CPROVER_requires(pp != NULL)"], + postconditions=["__CPROVER_ensures(__CPROVER_return_value == 0)"] + ) + expected_transformed_spec = transformer.move_preconditions_to_assigns(spec_with_no_assigns) + assert expected_transformed_spec == spec_with_no_assigns + def test_move_preconditions_to_assigns_conditional(): spec_with_preconditions = FunctionSpecification( preconditions=[ diff --git a/util/spec_transformer.py b/util/spec_transformer.py index 0b886503..efb5adab 100644 --- a/util/spec_transformer.py +++ b/util/spec_transformer.py @@ -61,7 +61,6 @@ def move_preconditions_to_assigns(self, spec: FunctionSpecification) -> Function return spec preconditions = [self._parser.parse(clause) for clause in spec.preconditions] - postconditions = [self._parser.parse(clause) for clause in spec.postconditions] precondition_exprs = [ clause.expr for clause in preconditions if isinstance(clause, RequiresClause) @@ -69,12 +68,18 @@ def move_preconditions_to_assigns(self, spec: FunctionSpecification) -> Function conjunction_of_preconditions_exprs = self._make_conjunction_from(precondition_exprs) updated_postconditions = [] + is_assigns_clause_updated = False for clause in postconditions: if isinstance(clause, Assigns): clause.condition = conjunction_of_preconditions_exprs + is_assigns_clause_updated = True updated_postconditions.append(clause.to_string()) - return FunctionSpecification(preconditions=[], postconditions=updated_postconditions) + return ( + FunctionSpecification(preconditions=[], postconditions=updated_postconditions) + if is_assigns_clause_updated + else spec + ) def move_preconditions_to_ensures(self, spec: FunctionSpecification) -> FunctionSpecification: """TODO: Implement me. From f917b9821103b649ed80d9f9ba5bd72bb71f050a Mon Sep 17 00:00:00 2001 From: James Yoo Date: Sat, 14 Feb 2026 16:25:41 -0800 Subject: [PATCH 03/18] Implementing `move_preconditions_to_ensures` --- test/util/test_spec_transformer.py | 33 +++++++- util/spec_transformer.py | 131 +++++++++++++++++++++++++---- 2 files changed, 144 insertions(+), 20 deletions(-) diff --git a/test/util/test_spec_transformer.py b/test/util/test_spec_transformer.py index 562327c1..69505f02 100644 --- a/test/util/test_spec_transformer.py +++ b/test/util/test_spec_transformer.py @@ -3,14 +3,43 @@ transformer = SpecTransformer() +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 = transformer.move_preconditions_to_ensures(spec_without_ensures) + 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)", + ], + postconditions=["__CPROVER_ensures(pp->p->buf[0] == 0)"], + ) + actual_transformed_spec = transformer.move_preconditions_to_ensures(spec_with_preconditions) + expected_transformed_spec = FunctionSpecification( + preconditions=[], + postconditions=[ + "__CPROVER_ensures(((pp->p->buf[0] == 0) || ((pp == NULL) || ((pp->p->buf == NULL) || (pp->p == NULL)))))" + ] + ) + assert actual_transformed_spec == expected_transformed_spec def test_move_preconditions_returns_unchanged_spec_if_no_assigns(): spec_with_no_assigns = FunctionSpecification( preconditions=["__CPROVER_requires(pp != NULL)"], postconditions=["__CPROVER_ensures(__CPROVER_return_value == 0)"] ) - expected_transformed_spec = transformer.move_preconditions_to_assigns(spec_with_no_assigns) - assert expected_transformed_spec == spec_with_no_assigns + actual_transformed_spec = transformer.move_preconditions_to_assigns(spec_with_no_assigns) + assert actual_transformed_spec == spec_with_no_assigns def test_move_preconditions_to_assigns_conditional(): spec_with_preconditions = FunctionSpecification( diff --git a/util/spec_transformer.py b/util/spec_transformer.py index efb5adab..e5be5f0e 100644 --- a/util/spec_transformer.py +++ b/util/spec_transformer.py @@ -1,6 +1,21 @@ """Class for applying transformations to specifications.""" -from translation.ast.cbmc_ast import AndOp, Assigns, CBMCAst, RequiresClause, ToAst +from translation.ast.cbmc_ast import ( + AndOp, + Assigns, + CBMCAst, + EnsuresClause, + EqOp, + GeOp, + GtOp, + LeOp, + LtOp, + NeqOp, + NotOp, + OrOp, + RequiresClause, + ToAst, +) from translation.parser import Parser from util import FunctionSpecification @@ -34,7 +49,7 @@ def move_preconditions_to_assigns(self, spec: FunctionSpecification) -> Function __CPROVER_assigns(pp->p->buf[0]) { if(pp && pp->p && pp->p->buf) - pp->p->buf[0] = 0; + pp->p->buf[0] = 0; } ``` @@ -65,7 +80,7 @@ def move_preconditions_to_assigns(self, spec: FunctionSpecification) -> Function precondition_exprs = [ clause.expr for clause in preconditions if isinstance(clause, RequiresClause) ] - conjunction_of_preconditions_exprs = self._make_conjunction_from(precondition_exprs) + conjunction_of_preconditions_exprs = self._apply_logical_op(precondition_exprs, AndOp) updated_postconditions = [] is_assigns_clause_updated = False @@ -82,18 +97,67 @@ def move_preconditions_to_assigns(self, spec: FunctionSpecification) -> Function ) def move_preconditions_to_ensures(self, spec: FunctionSpecification) -> FunctionSpecification: - """TODO: Implement me. + """Return a spec where precondition exprs are moved to disjunctions for ensures clauses. - Args: - spec (FunctionSpecification): _description_ + There are cases where a specification might contain preconditions that are *too* strong, + effectively weakening the entire specification. Below is one example: + + ```c + void f1(struct pair_of_pairs *pp) + __CPROVER_requires(pp != NULL) + __CPROVER_requires(pp->p != NULL) + __CPROVER_requires(pp->p->buf != NULL) + __CPROVER_ensures(pp->p->buf[0] == 0) + { + if(pp && pp->p && pp->p->buf) + pp->p->buf[0] = 0; + } + ``` - Raises: - NotImplementedError: _description_ + It is the case that `f1` might be called with a NULL `pp` (or `pp->p` or `pp->p->buf`), and + the function accounts for this with a conditional check. A more expressive spec is: + + __CPROVER_ensures( + pp == NULL || pp->p == NULL || pp->p->buf == NULL || pp->p->buf[0] == 0 + ) + + Args: + spec (FunctionSpecification): The specification. Returns: - FunctionSpecification: _description_ + FunctionSpecification: The specification, where each precondition expression is moved + to a disjunction in ensures clauses. """ - raise NotImplementedError("TODO") + if not spec.preconditions: + return spec + + preconditions = [self._parser.parse(clause) for clause in spec.preconditions] + postconditions = [self._parser.parse(clause) for clause in spec.postconditions] + negated_precondition_exprs = [ + self._negate(clause.expr) + 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 + for clause in postconditions: + if isinstance(clause, EnsuresClause): + updated_ensures_expr = self._apply_logical_op( + [disjunction_of_negated_precondition_exprs, clause.expr], OrOp + ) + clause.expr = updated_ensures_expr + is_ensures_clause_updated = True + updated_postconditions.append(clause.to_string()) + + return ( + FunctionSpecification(preconditions=[], postconditions=updated_postconditions) + if is_ensures_clause_updated + else spec + ) def _get_assigns_clauses(self, spec: FunctionSpecification) -> list[Assigns]: """Return the Assigns clauses in a specification. @@ -107,19 +171,50 @@ def _get_assigns_clauses(self, spec: FunctionSpecification) -> list[Assigns]: parsed_postconditions = [self._parser.parse(clause) for clause in spec.postconditions] return [clause for clause in parsed_postconditions if isinstance(clause, Assigns)] - def _make_conjunction_from(self, exprs: list[CBMCAst]) -> CBMCAst: - """Return a conjunction (i.e., an AndOp) comprising the given expressions. + def _apply_logical_op(self, exprs: list[CBMCAst], logical_op: type[AndOp | OrOp]) -> CBMCAst: + """Return the result of applying a logical operation between each expr. Args: - exprs (list[CBMCAst]): The expressions to construct a conjunction from. + exprs (list[CBMCAst]): The exprs to which to apply the logical operation. + logical_op (type[AndOp | OrOp]): The logical operation. Returns: - CBMCAst: The conjunction. + CBMCAst: The result of applying the logical operation. """ if len(exprs) == 1: return exprs[0] - conjunction = AndOp(left=exprs.pop(), right=exprs.pop()) - andop = conjunction + result = logical_op(left=exprs.pop(), right=exprs.pop()) while exprs: - andop = AndOp(left=exprs.pop(), right=andop) - return andop + result = logical_op(left=exprs.pop(), right=result) + return result + + def _negate(self, expr: CBMCAst) -> CBMCAst: + """Return the negated expr. + + Args: + expr (CBMCAst): The expr to negate. + + Returns: + CBMCAst: The negated expr. + """ + match expr: + case AndOp(left, right): + return OrOp(left=self._negate(left), right=self._negate(right)) + case OrOp(left, right): + return AndOp(left=self._negate(left), right=self._negate(right)) + case NotOp(operand): + return operand + case EqOp(left, right): + return NeqOp(left, right) + case NeqOp(left, right): + return EqOp(left, right) + case GtOp(left, right): + return LeOp(left, right) + case GeOp(left, right): + return LtOp(left, right) + case LtOp(left, right): + return GeOp(left, right) + case LeOp(left, right): + return GtOp(left, right) + case _: + return expr From c31a153d2c12625c738c8e50f2318867ab5dc035 Mon Sep 17 00:00:00 2001 From: James Yoo Date: Sun, 15 Feb 2026 10:36:55 -0800 Subject: [PATCH 04/18] Addressing CodeRabbit comments --- test/util/test_spec_transformer.py | 7 ++++--- util/spec_transformer.py | 30 ++++++++++++++++++++---------- 2 files changed, 24 insertions(+), 13 deletions(-) diff --git a/test/util/test_spec_transformer.py b/test/util/test_spec_transformer.py index 69505f02..501fac10 100644 --- a/test/util/test_spec_transformer.py +++ b/test/util/test_spec_transformer.py @@ -6,7 +6,6 @@ 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)", ], @@ -21,14 +20,16 @@ def test_move_preconditions_to_ensures_disjunctions(): "__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 = transformer.move_preconditions_to_ensures(spec_with_preconditions) + print(actual_transformed_spec) expected_transformed_spec = FunctionSpecification( preconditions=[], postconditions=[ - "__CPROVER_ensures(((pp->p->buf[0] == 0) || ((pp == NULL) || ((pp->p->buf == NULL) || (pp->p == NULL)))))" + "__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 @@ -53,7 +54,7 @@ def test_move_preconditions_to_assigns_conditional(): expected_transformed_spec = FunctionSpecification( preconditions=[], postconditions=[ - "__CPROVER_assigns(((pp != NULL) && ((pp->p->buf != NULL) && (pp->p != NULL))) : pp->p->buf[0])" + "__CPROVER_assigns((((pp != NULL) && (pp->p != NULL)) && (pp->p->buf != NULL)) : pp->p->buf[0])" ], ) actual_transformed_spec = transformer.move_preconditions_to_assigns(spec_with_preconditions) diff --git a/util/spec_transformer.py b/util/spec_transformer.py index e5be5f0e..1624cd88 100644 --- a/util/spec_transformer.py +++ b/util/spec_transformer.py @@ -3,6 +3,7 @@ from translation.ast.cbmc_ast import ( AndOp, Assigns, + CallOp, CBMCAst, EnsuresClause, EqOp, @@ -28,11 +29,15 @@ class SpecTransformer: """ - _parser: Parser[CBMCAst] = Parser( - path_to_grammar_defn="translation/grammar/cbmc.txt", - start="cbmc_clause", - transformer=ToAst(), - ) + _parser: Parser[CBMCAst] + + def __init__(self): + """Create a new SpecTransformer.""" + self._parser = Parser( + path_to_grammar_defn="translation/grammar/cbmc.txt", + start="cbmc_clause", + transformer=ToAst(), + ) def move_preconditions_to_assigns(self, spec: FunctionSpecification) -> FunctionSpecification: """Return a spec where precondition expressions are moved to conditions for assigns clauses. @@ -181,11 +186,12 @@ def _apply_logical_op(self, exprs: list[CBMCAst], logical_op: type[AndOp | OrOp] Returns: CBMCAst: The result of applying the logical operation. """ - if len(exprs) == 1: - return exprs[0] - result = logical_op(left=exprs.pop(), right=exprs.pop()) - while exprs: - result = logical_op(left=exprs.pop(), right=result) + if not exprs: + msg = f"{logical_op} cannot be applied to an empty list of expressions" + raise ValueError(msg) + result = exprs[0] + for expr in exprs[1:]: + result = logical_op(left=result, right=expr) return result def _negate(self, expr: CBMCAst) -> CBMCAst: @@ -216,5 +222,9 @@ def _negate(self, expr: CBMCAst) -> CBMCAst: return GeOp(left, right) case LeOp(left, right): return GtOp(left, right) + case CallOp(_, _): + # This assumes that any method calls in a precondition return booleans. + # Fine for now, but may have to come back later. + return NotOp(expr) case _: return expr From 1dc0a61a68f7049214745312e0c7b799ee3595ed Mon Sep 17 00:00:00 2001 From: James Yoo Date: Sun, 15 Feb 2026 10:55:06 -0800 Subject: [PATCH 05/18] Removing debug statement --- test/util/test_spec_transformer.py | 1 - 1 file changed, 1 deletion(-) diff --git a/test/util/test_spec_transformer.py b/test/util/test_spec_transformer.py index 501fac10..6602ce78 100644 --- a/test/util/test_spec_transformer.py +++ b/test/util/test_spec_transformer.py @@ -25,7 +25,6 @@ def test_move_preconditions_to_ensures_disjunctions(): postconditions=["__CPROVER_ensures(pp->p->buf[0] == 0)"], ) actual_transformed_spec = transformer.move_preconditions_to_ensures(spec_with_preconditions) - print(actual_transformed_spec) expected_transformed_spec = FunctionSpecification( preconditions=[], postconditions=[ From 6e1931474b4e12bdc862b09716dc95b85594f5a3 Mon Sep 17 00:00:00 2001 From: James Yoo Date: Thu, 19 Feb 2026 14:27:08 -0800 Subject: [PATCH 06/18] Making `negate()` a method defined on `CBMCAst` --- translation/ast/cbmc_ast.py | 38 ++++++++++++++++++++++++++++++ util/spec_transformer.py | 47 +------------------------------------ 2 files changed, 39 insertions(+), 46 deletions(-) diff --git a/translation/ast/cbmc_ast.py b/translation/ast/cbmc_ast.py index 3d627142..f7092bfa 100644 --- a/translation/ast/cbmc_ast.py +++ b/translation/ast/cbmc_ast.py @@ -25,6 +25,14 @@ def to_string(self) -> str: """ raise NotImplementedError(f"to_string not implemented for {type(self).__name__}") + def negate(self) -> "CBMCAst": + """Return the negation of this AST node. + + Returns: + CBMCAst: The negation of this AST node. + """ + raise NotImplementedError(f"negate not implemented for {type(self).__name__}") + def _to_str(node: Any) -> str: """Convert an AST node or primitive value to a string. @@ -144,6 +152,9 @@ class OrOp(BinOp): def operator(self) -> str: return "||" + def negate(self) -> CBMCAst: + return AndOp(left=self.left.negate(), right=self.right.negate()) + @dataclass class AndOp(BinOp): @@ -153,6 +164,9 @@ class AndOp(BinOp): def operator(self) -> str: return "&&" + def negate(self) -> CBMCAst: + return OrOp(left=self.left.negate(), right=self.right.negate()) + @dataclass class EqOp(BinOp): @@ -162,6 +176,9 @@ class EqOp(BinOp): def operator(self) -> str: return "==" + def negate(self) -> CBMCAst: + return NeqOp(left=self.left, right=self.right) + @dataclass class NeqOp(BinOp): @@ -171,6 +188,9 @@ class NeqOp(BinOp): def operator(self) -> str: return "!=" + def negate(self) -> CBMCAst: + return EqOp(left=self.left, right=self.right) + @dataclass class LtOp(BinOp): @@ -180,6 +200,9 @@ class LtOp(BinOp): def operator(self) -> str: return "<" + def negate(self) -> CBMCAst: + return GeOp(left=self.left, right=self.right) + @dataclass class LeOp(BinOp): @@ -189,6 +212,9 @@ class LeOp(BinOp): def operator(self) -> str: return "<=" + def negate(self) -> CBMCAst: + return GtOp(left=self.left, right=self.right) + @dataclass class GtOp(BinOp): @@ -198,6 +224,9 @@ class GtOp(BinOp): def operator(self) -> str: return ">" + def negate(self) -> CBMCAst: + return LeOp(left=self.left, right=self.right) + @dataclass class GeOp(BinOp): @@ -207,6 +236,9 @@ class GeOp(BinOp): def operator(self) -> str: return ">=" + def negate(self) -> CBMCAst: + return LtOp(left=self.left, right=self.right) + @dataclass class AddOp(BinOp): @@ -260,6 +292,9 @@ class NotOp(CBMCAst): def to_string(self) -> str: return f"!{_to_str(self.operand)}" + def negate(self) -> CBMCAst: + return self.operand + @dataclass class AddrOp(CBMCAst): @@ -330,6 +365,9 @@ class CallOp(CBMCAst): def to_string(self) -> str: return f"{_to_str(self.func)}({_to_str(self.args)})" + def negate(self) -> CBMCAst: + return NotOp(self) + @dataclass class ArgList(CBMCAst, ast_utils.AsList): diff --git a/util/spec_transformer.py b/util/spec_transformer.py index 1624cd88..22f2edb9 100644 --- a/util/spec_transformer.py +++ b/util/spec_transformer.py @@ -3,16 +3,8 @@ from translation.ast.cbmc_ast import ( AndOp, Assigns, - CallOp, CBMCAst, EnsuresClause, - EqOp, - GeOp, - GtOp, - LeOp, - LtOp, - NeqOp, - NotOp, OrOp, RequiresClause, ToAst, @@ -139,9 +131,7 @@ def move_preconditions_to_ensures(self, spec: FunctionSpecification) -> Function preconditions = [self._parser.parse(clause) for clause in spec.preconditions] postconditions = [self._parser.parse(clause) for clause in spec.postconditions] negated_precondition_exprs = [ - self._negate(clause.expr) - for clause in preconditions - if isinstance(clause, RequiresClause) + clause.expr.negate() for clause in preconditions if isinstance(clause, RequiresClause) ] disjunction_of_negated_precondition_exprs = self._apply_logical_op( negated_precondition_exprs, OrOp @@ -193,38 +183,3 @@ def _apply_logical_op(self, exprs: list[CBMCAst], logical_op: type[AndOp | OrOp] for expr in exprs[1:]: result = logical_op(left=result, right=expr) return result - - def _negate(self, expr: CBMCAst) -> CBMCAst: - """Return the negated expr. - - Args: - expr (CBMCAst): The expr to negate. - - Returns: - CBMCAst: The negated expr. - """ - match expr: - case AndOp(left, right): - return OrOp(left=self._negate(left), right=self._negate(right)) - case OrOp(left, right): - return AndOp(left=self._negate(left), right=self._negate(right)) - case NotOp(operand): - return operand - case EqOp(left, right): - return NeqOp(left, right) - case NeqOp(left, right): - return EqOp(left, right) - case GtOp(left, right): - return LeOp(left, right) - case GeOp(left, right): - return LtOp(left, right) - case LtOp(left, right): - return GeOp(left, right) - case LeOp(left, right): - return GtOp(left, right) - case CallOp(_, _): - # This assumes that any method calls in a precondition return booleans. - # Fine for now, but may have to come back later. - return NotOp(expr) - case _: - return expr From d58429c0bdf1f047a13d7f6b9012f89f46f22c94 Mon Sep 17 00:00:00 2001 From: James Yoo Date: Thu, 19 Feb 2026 14:43:12 -0800 Subject: [PATCH 07/18] Applying some fixes --- translation/ast/cbmc_ast.py | 7 +++---- util/spec_transformer.py | 14 +------------- 2 files changed, 4 insertions(+), 17 deletions(-) diff --git a/translation/ast/cbmc_ast.py b/translation/ast/cbmc_ast.py index f7092bfa..ad19cff6 100644 --- a/translation/ast/cbmc_ast.py +++ b/translation/ast/cbmc_ast.py @@ -28,10 +28,12 @@ def to_string(self) -> str: 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. """ - raise NotImplementedError(f"negate not implemented for {type(self).__name__}") + return NotOp(self) def _to_str(node: Any) -> str: @@ -365,9 +367,6 @@ class CallOp(CBMCAst): def to_string(self) -> str: return f"{_to_str(self.func)}({_to_str(self.args)})" - def negate(self) -> CBMCAst: - return NotOp(self) - @dataclass class ArgList(CBMCAst, ast_utils.AsList): diff --git a/util/spec_transformer.py b/util/spec_transformer.py index 22f2edb9..2ee2685b 100644 --- a/util/spec_transformer.py +++ b/util/spec_transformer.py @@ -23,7 +23,7 @@ class SpecTransformer: _parser: Parser[CBMCAst] - def __init__(self): + def __init__(self) -> None: """Create a new SpecTransformer.""" self._parser = Parser( path_to_grammar_defn="translation/grammar/cbmc.txt", @@ -154,18 +154,6 @@ def move_preconditions_to_ensures(self, spec: FunctionSpecification) -> Function else spec ) - def _get_assigns_clauses(self, spec: FunctionSpecification) -> list[Assigns]: - """Return the Assigns clauses in a specification. - - Args: - spec (FunctionSpecification): The specification. - - Returns: - list[Assigns]: The Assigns clauses in a specification. - """ - parsed_postconditions = [self._parser.parse(clause) for clause in spec.postconditions] - return [clause for clause in parsed_postconditions if isinstance(clause, Assigns)] - def _apply_logical_op(self, exprs: list[CBMCAst], logical_op: type[AndOp | OrOp]) -> CBMCAst: """Return the result of applying a logical operation between each expr. From 15e067de25463a45f54838d5931629675e7c556c Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Thu, 19 Feb 2026 16:57:37 -0800 Subject: [PATCH 08/18] Tweak comments --- util/spec_transformer.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/util/spec_transformer.py b/util/spec_transformer.py index 1624cd88..433a799e 100644 --- a/util/spec_transformer.py +++ b/util/spec_transformer.py @@ -119,7 +119,7 @@ def move_preconditions_to_ensures(self, spec: FunctionSpecification) -> Function } ``` - It is the case that `f1` might be called with a NULL `pp` (or `pp->p` or `pp->p->buf`), and + Function `f1` might be called with a NULL `pp` (or `pp->p` or `pp->p->buf`), and the function accounts for this with a conditional check. A more expressive spec is: __CPROVER_ensures( @@ -181,7 +181,7 @@ def _apply_logical_op(self, exprs: list[CBMCAst], logical_op: type[AndOp | OrOp] Args: exprs (list[CBMCAst]): The exprs to which to apply the logical operation. - logical_op (type[AndOp | OrOp]): The logical operation. + logical_op (type[AndOp | OrOp]): The logical operation. Returns: CBMCAst: The result of applying the logical operation. From d533dcefb52caa5b92fc8fe33da6a16d1740365e Mon Sep 17 00:00:00 2001 From: James Yoo Date: Sun, 22 Feb 2026 11:10:07 -0800 Subject: [PATCH 09/18] Addressing more CodeRabbit comments --- util/spec_transformer.py | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/util/spec_transformer.py b/util/spec_transformer.py index 2ee2685b..61578f5c 100644 --- a/util/spec_transformer.py +++ b/util/spec_transformer.py @@ -73,17 +73,16 @@ def move_preconditions_to_assigns(self, spec: FunctionSpecification) -> Function return spec preconditions = [self._parser.parse(clause) for clause in spec.preconditions] - postconditions = [self._parser.parse(clause) for clause in spec.postconditions] precondition_exprs = [ clause.expr for clause in preconditions if isinstance(clause, RequiresClause) ] - conjunction_of_preconditions_exprs = self._apply_logical_op(precondition_exprs, AndOp) + postconditions = [self._parser.parse(clause) for clause in spec.postconditions] updated_postconditions = [] is_assigns_clause_updated = False for clause in postconditions: if isinstance(clause, Assigns): - clause.condition = conjunction_of_preconditions_exprs + clause.condition = self._apply_logical_op(precondition_exprs, AndOp) is_assigns_clause_updated = True updated_postconditions.append(clause.to_string()) From ecc8b0f992f91c48e7fb152d19127d5e7533431e Mon Sep 17 00:00:00 2001 From: James Yoo Date: Sun, 22 Feb 2026 13:36:49 -0800 Subject: [PATCH 10/18] Creating explicit variant generation module --- specifications/__init__.py | 3 +- specifications/variants/__init__.py | 3 + .../variants/specification_variant_factory.py | 32 ++++ .../variants/transformations/__init__.py | 4 + ...ve_preconditions_to_assigns_and_ensures.py | 89 +++++++++ .../specification_transformation.py | 50 +++++ test/specifications/__init__.py | 0 .../transformations/__init__.py | 0 ...e_preconditions_to_assigns_and_ensures.py} | 32 ++-- util/spec_transformer.py | 172 ------------------ 10 files changed, 194 insertions(+), 191 deletions(-) create mode 100644 specifications/variants/__init__.py create mode 100644 specifications/variants/specification_variant_factory.py create mode 100644 specifications/variants/transformations/__init__.py create mode 100644 specifications/variants/transformations/move_preconditions_to_assigns_and_ensures.py create mode 100644 specifications/variants/transformations/specification_transformation.py create mode 100644 test/specifications/__init__.py create mode 100644 test/specifications/transformations/__init__.py rename test/{util/test_spec_transformer.py => specifications/transformations/test_move_preconditions_to_assigns_and_ensures.py} (59%) delete mode 100644 util/spec_transformer.py diff --git a/specifications/__init__.py b/specifications/__init__.py index 52858e83..5bf6262e 100644 --- a/specifications/__init__.py +++ b/specifications/__init__.py @@ -1,4 +1,5 @@ from .llm_specification_generator import LlmSpecificationGenerator from .specification_extractor import extract_spec_from_response +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 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..429d103c --- /dev/null +++ b/specifications/variants/specification_variant_factory.py @@ -0,0 +1,32 @@ +"""Class for symbolically generating variants of a specification.""" + +from util import FunctionSpecification + +from .transformations import MovePreconditionsToAssignsAndEnsures, 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(),) + + 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) diff --git a/specifications/variants/transformations/__init__.py b/specifications/variants/transformations/__init__.py new file mode 100644 index 00000000..efa1a82e --- /dev/null +++ b/specifications/variants/transformations/__init__.py @@ -0,0 +1,4 @@ +from .specification_transformation import SpecificationTransformation +from .move_preconditions_to_assigns_and_ensures import MovePreconditionsToAssignsAndEnsures + +__all__ = ["SpecificationTransformation", "MovePreconditionsToAssignsAndEnsures"] \ No newline at end of file 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..3607d905 --- /dev/null +++ b/specifications/variants/transformations/move_preconditions_to_assigns_and_ensures.py @@ -0,0 +1,89 @@ +"""Transformation where expressions in preconditions are moved to assigns and ensures clauses.""" + +from translation.ast.cbmc_ast import ( + AndOp, + Assigns, + CBMCAst, + EnsuresClause, + OrOp, + RequiresClause, + ToAst, +) +from translation.parser import Parser +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 __init__(self) -> None: + """Create a new MovePreconditionsToAssignsAndEnsures.""" + self._parser = Parser( + path_to_grammar_defn="translation/grammar/cbmc.txt", + start="cbmc_clause", + transformer=ToAst(), + ) + + def apply(self, specification: FunctionSpecification) -> 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: + FunctionSpecification: The transformed specification. + """ + preconditions_ast, postconditions_ast = self._parse_specification(specification) + + # If there are no postconditions, return unchanged. + if not postconditions_ast: + return specification + + # Extract the inner expressions from each RequiresClause. + precondition_exprs: list[CBMCAst] = [ + clause.expr for clause in preconditions_ast 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 postconditions_ast: + 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/specification_transformation.py b/specifications/variants/transformations/specification_transformation.py new file mode 100644 index 00000000..bf0eb8e2 --- /dev/null +++ b/specifications/variants/transformations/specification_transformation.py @@ -0,0 +1,50 @@ +"""Represent a transformation of a specification.""" + +from abc import ABC, abstractmethod + +from translation.ast.cbmc_ast import ( + CBMCAst, +) +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] + + @abstractmethod + def apply(self, specification: FunctionSpecification) -> FunctionSpecification: + """Return the result of applying this transformation to the given specification. + + Args: + specification (FunctionSpecification): The specification to which to apply this + transformation + + Returns: + FunctionSpecification: The result 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/util/test_spec_transformer.py b/test/specifications/transformations/test_move_preconditions_to_assigns_and_ensures.py similarity index 59% rename from test/util/test_spec_transformer.py rename to test/specifications/transformations/test_move_preconditions_to_assigns_and_ensures.py index 6602ce78..5ce84eeb 100644 --- a/test/util/test_spec_transformer.py +++ b/test/specifications/transformations/test_move_preconditions_to_assigns_and_ensures.py @@ -1,7 +1,8 @@ -from util.spec_transformer import SpecTransformer +from specifications.variants.transformations import MovePreconditionsToAssignsAndEnsures from util import FunctionSpecification -transformer = SpecTransformer() +transformation = MovePreconditionsToAssignsAndEnsures() + def test_move_preconditions_to_ensures_returns_unchanged_specs_if_no_ensures_clause(): spec_without_ensures = FunctionSpecification( @@ -9,11 +10,12 @@ def test_move_preconditions_to_ensures_returns_unchanged_specs_if_no_ensures_cla "__CPROVER_requires(pp->p != NULL)", "__CPROVER_requires(pp->p->buf != NULL)", ], - postconditions=[] + postconditions=[], ) - actual_transformed_spec = transformer.move_preconditions_to_ensures(spec_without_ensures) + actual_transformed_spec = transformation.apply(spec_without_ensures) assert actual_transformed_spec == spec_without_ensures + def test_move_preconditions_to_ensures_disjunctions(): spec_with_preconditions = FunctionSpecification( preconditions=[ @@ -24,37 +26,31 @@ def test_move_preconditions_to_ensures_disjunctions(): ], postconditions=["__CPROVER_ensures(pp->p->buf[0] == 0)"], ) - actual_transformed_spec = transformer.move_preconditions_to_ensures(spec_with_preconditions) + 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)) || !some_call(foo)) || (pp->p->buf[0] == 0)))" - ] + ], ) assert actual_transformed_spec == expected_transformed_spec -def test_move_preconditions_returns_unchanged_spec_if_no_assigns(): - spec_with_no_assigns = FunctionSpecification( - preconditions=["__CPROVER_requires(pp != NULL)"], - postconditions=["__CPROVER_ensures(__CPROVER_return_value == 0)"] - ) - actual_transformed_spec = transformer.move_preconditions_to_assigns(spec_with_no_assigns) - assert actual_transformed_spec == spec_with_no_assigns -def test_move_preconditions_to_assigns_conditional(): +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_assigns(pp->p->buf[0])"], + 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_assigns((((pp != NULL) && (pp->p != NULL)) && (pp->p->buf != NULL)) : pp->p->buf[0])" + "__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)", ], ) - actual_transformed_spec = transformer.move_preconditions_to_assigns(spec_with_preconditions) - assert expected_transformed_spec == actual_transformed_spec + assert actual_transformed_spec == expected_transformed_spec diff --git a/util/spec_transformer.py b/util/spec_transformer.py deleted file mode 100644 index 3fd0d410..00000000 --- a/util/spec_transformer.py +++ /dev/null @@ -1,172 +0,0 @@ -"""Class for applying transformations to specifications.""" - -from translation.ast.cbmc_ast import ( - AndOp, - Assigns, - CBMCAst, - EnsuresClause, - OrOp, - RequiresClause, - ToAst, -) -from translation.parser import Parser -from util import FunctionSpecification - - -class SpecTransformer: - """Class for applying transformations to specifications. - - Attributes: - (_parser): Parser[CBMCAst]: A parser for CBMC specifications. - - """ - - _parser: Parser[CBMCAst] - - def __init__(self) -> None: - """Create a new SpecTransformer.""" - self._parser = Parser( - path_to_grammar_defn="translation/grammar/cbmc.txt", - start="cbmc_clause", - transformer=ToAst(), - ) - - def move_preconditions_to_assigns(self, spec: FunctionSpecification) -> FunctionSpecification: - """Return a spec where precondition expressions are moved to conditions for assigns clauses. - - There are cases where a specification might contain preconditions that are *too* strong, - effectively weakening the entire specification. Below is one example: - - ```c - void f1(struct pair_of_pairs *pp) - __CPROVER_requires(pp != NULL) - __CPROVER_requires(pp->p != NULL) - __CPROVER_requires(pp->p->buf != NULL) - __CPROVER_ensures(pp->p->buf[0] == 0) - __CPROVER_assigns(pp->p->buf[0]) - { - if(pp && pp->p && pp->p->buf) - pp->p->buf[0] = 0; - } - ``` - - It is the case that `f1` might be called with a NULL `pp` (or `pp->p` or `pp->p->buf`), and - the function accounts for this with a conditional check. A more expressive and accurate - specification would be: - - __CPROVER_ensures(pp->p->buf[0] == 0) - __CPROVER_assigns( - pp != NULL && pp->p != NULL && pp->p->buf != NULL : pp->p->buf[0] - ) - - Where each expression in a precondition is provided as a condition for the assignment - `pp->p->buf[0]`. - - Args: - spec (FunctionSpecification): The specification. - - Returns: - FunctionSpecification: The specification, where each precondition expression is moved - to a condition for assignment clauses. - """ - if not spec.preconditions: - return spec - - preconditions = [self._parser.parse(clause) for clause in spec.preconditions] - precondition_exprs = [ - clause.expr for clause in preconditions if isinstance(clause, RequiresClause) - ] - postconditions = [self._parser.parse(clause) for clause in spec.postconditions] - - updated_postconditions = [] - is_assigns_clause_updated = False - for clause in postconditions: - if isinstance(clause, Assigns): - clause.condition = self._apply_logical_op(precondition_exprs, AndOp) - is_assigns_clause_updated = True - updated_postconditions.append(clause.to_string()) - - return ( - FunctionSpecification(preconditions=[], postconditions=updated_postconditions) - if is_assigns_clause_updated - else spec - ) - - def move_preconditions_to_ensures(self, spec: FunctionSpecification) -> FunctionSpecification: - """Return a spec where precondition exprs are moved to disjunctions for ensures clauses. - - There are cases where a specification might contain preconditions that are *too* strong, - effectively weakening the entire specification. Below is one example: - - ```c - void f1(struct pair_of_pairs *pp) - __CPROVER_requires(pp != NULL) - __CPROVER_requires(pp->p != NULL) - __CPROVER_requires(pp->p->buf != NULL) - __CPROVER_ensures(pp->p->buf[0] == 0) - { - if(pp && pp->p && pp->p->buf) - pp->p->buf[0] = 0; - } - ``` - - Function `f1` might be called with a NULL `pp` (or `pp->p` or `pp->p->buf`), and - the function accounts for this with a conditional check. A more expressive spec is: - - __CPROVER_ensures( - pp == NULL || pp->p == NULL || pp->p->buf == NULL || pp->p->buf[0] == 0 - ) - - Args: - spec (FunctionSpecification): The specification. - - Returns: - FunctionSpecification: The specification, where each precondition expression is moved - to a disjunction in ensures clauses. - """ - if not spec.preconditions: - return spec - - 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 - ) - - updated_postconditions = [] - is_ensures_clause_updated = False - for clause in postconditions: - if isinstance(clause, EnsuresClause): - updated_ensures_expr = self._apply_logical_op( - [disjunction_of_negated_precondition_exprs, clause.expr], OrOp - ) - clause.expr = updated_ensures_expr - is_ensures_clause_updated = True - updated_postconditions.append(clause.to_string()) - - return ( - FunctionSpecification(preconditions=[], postconditions=updated_postconditions) - if is_ensures_clause_updated - else spec - ) - - def _apply_logical_op(self, exprs: list[CBMCAst], logical_op: type[AndOp | OrOp]) -> CBMCAst: - """Return the result of applying a logical operation between each expr. - - Args: - exprs (list[CBMCAst]): The exprs to which to apply the logical operation. - logical_op (type[AndOp | OrOp]): The logical operation. - - Returns: - CBMCAst: The result of applying the logical operation. - """ - if not exprs: - msg = f"{logical_op} cannot be applied to an empty list of expressions" - raise ValueError(msg) - result = exprs[0] - for expr in exprs[1:]: - result = logical_op(left=result, right=expr) - return result From 4198627d87a3fc532d807db0fe20ebbce8d78c94 Mon Sep 17 00:00:00 2001 From: James Yoo Date: Sun, 22 Feb 2026 14:21:08 -0800 Subject: [PATCH 11/18] Adding transformation to remove preconditions --- .../variants/specification_variant_factory.py | 5 +- .../variants/transformations/__init__.py | 3 +- ...ve_preconditions_to_assigns_and_ensures.py | 27 ++++--- .../transformations/remove_preconditions.py | 73 +++++++++++++++++++ .../specification_transformation.py | 6 +- ...ve_preconditions_to_assigns_and_ensures.py | 6 +- .../test_remove_preconditions.py | 39 ++++++++++ 7 files changed, 139 insertions(+), 20 deletions(-) create mode 100644 specifications/variants/transformations/remove_preconditions.py create mode 100644 test/specifications/transformations/test_remove_preconditions.py diff --git a/specifications/variants/specification_variant_factory.py b/specifications/variants/specification_variant_factory.py index 429d103c..bb45af7d 100644 --- a/specifications/variants/specification_variant_factory.py +++ b/specifications/variants/specification_variant_factory.py @@ -29,4 +29,7 @@ def get_variants(self, spec: FunctionSpecification) -> tuple[FunctionSpecificati Returns: tuple[FunctionSpecification, ...]: The variants of the given specification. """ - return tuple(transformation.apply(spec) for transformation in self._transformations) + 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 index efa1a82e..21cd4a7a 100644 --- a/specifications/variants/transformations/__init__.py +++ b/specifications/variants/transformations/__init__.py @@ -1,4 +1,5 @@ from .specification_transformation import SpecificationTransformation from .move_preconditions_to_assigns_and_ensures import MovePreconditionsToAssignsAndEnsures +from .remove_preconditions import RemovePreconditions -__all__ = ["SpecificationTransformation", "MovePreconditionsToAssignsAndEnsures"] \ No newline at end of file +__all__ = ["SpecificationTransformation", "MovePreconditionsToAssignsAndEnsures", "RemovePreconditions"] \ No newline at end of file diff --git a/specifications/variants/transformations/move_preconditions_to_assigns_and_ensures.py b/specifications/variants/transformations/move_preconditions_to_assigns_and_ensures.py index 3607d905..82ad29c2 100644 --- a/specifications/variants/transformations/move_preconditions_to_assigns_and_ensures.py +++ b/specifications/variants/transformations/move_preconditions_to_assigns_and_ensures.py @@ -31,7 +31,7 @@ def __init__(self) -> None: transformer=ToAst(), ) - def apply(self, specification: FunctionSpecification) -> FunctionSpecification: + 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: @@ -42,25 +42,26 @@ def apply(self, specification: FunctionSpecification) -> FunctionSpecification: specification (FunctionSpecification): The specification to transform. Returns: - FunctionSpecification: The transformed specification. + list[FunctionSpecification]: The result of applying this transformation to the given + specification. """ - preconditions_ast, postconditions_ast = self._parse_specification(specification) + precondition_asts, postcondition_asts = self._parse_specification(specification) # If there are no postconditions, return unchanged. - if not postconditions_ast: - return specification + if not postcondition_asts: + return [specification] # Extract the inner expressions from each RequiresClause. precondition_exprs: list[CBMCAst] = [ - clause.expr for clause in preconditions_ast if isinstance(clause, RequiresClause) + 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 + return [specification] new_postconditions: list[str] = [] - for post_ast in postconditions_ast: + for post_ast in postcondition_asts: if isinstance(post_ast, EnsuresClause): # Build disjunction: !pre1 || !pre2 || ... || ensures_expr result: CBMCAst = precondition_exprs[0].negate() @@ -83,7 +84,9 @@ def apply(self, specification: FunctionSpecification) -> FunctionSpecification: else: new_postconditions.append(post_ast.to_string()) - return FunctionSpecification( - preconditions=[], - postconditions=new_postconditions, - ) + 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..fc4be124 --- /dev/null +++ b/specifications/variants/transformations/remove_preconditions.py @@ -0,0 +1,73 @@ +"""Transformation where preconditions are removed, one-by-one.""" + +from translation.ast.cbmc_ast import ( + ToAst, +) +from translation.parser import Parser +from util import FunctionSpecification + +from .specification_transformation import SpecificationTransformation + + +class RemovePreconditions(SpecificationTransformation): + """Transformation where precondition expressions are removed one-by-one.""" + + def __init__(self) -> None: + """Create a new RemovePreconditions.""" + self._parser = Parser( + path_to_grammar_defn="translation/grammar/cbmc.txt", + start="cbmc_clause", + transformer=ToAst(), + ) + + 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 index bf0eb8e2..bcde785f 100644 --- a/specifications/variants/transformations/specification_transformation.py +++ b/specifications/variants/transformations/specification_transformation.py @@ -19,15 +19,15 @@ class SpecificationTransformation(ABC): _parser: Parser[CBMCAst] @abstractmethod - def apply(self, specification: FunctionSpecification) -> FunctionSpecification: - """Return the result of applying this transformation to the given specification. + 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: - FunctionSpecification: The result of applying this specification to the given + list[FunctionSpecification]: The result(s) of applying this specification to the given specification. """ ... 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 index 5ce84eeb..8d03e357 100644 --- a/test/specifications/transformations/test_move_preconditions_to_assigns_and_ensures.py +++ b/test/specifications/transformations/test_move_preconditions_to_assigns_and_ensures.py @@ -12,7 +12,7 @@ def test_move_preconditions_to_ensures_returns_unchanged_specs_if_no_ensures_cla ], postconditions=[], ) - actual_transformed_spec = transformation.apply(spec_without_ensures) + actual_transformed_spec = transformation.apply(spec_without_ensures)[0] assert actual_transformed_spec == spec_without_ensures @@ -26,7 +26,7 @@ def test_move_preconditions_to_ensures_disjunctions(): ], postconditions=["__CPROVER_ensures(pp->p->buf[0] == 0)"], ) - actual_transformed_spec = transformation.apply(spec_with_preconditions) + actual_transformed_spec = transformation.apply(spec_with_preconditions)[0] expected_transformed_spec = FunctionSpecification( preconditions=[], postconditions=[ @@ -45,7 +45,7 @@ def test_move_preconditions_to_ensures_disjunctions_and_assigns_conditions(): ], postconditions=["__CPROVER_ensures(pp->p->buf[0] == 0)", "__CPROVER_assigns(pp->p->buf)"], ) - actual_transformed_spec = transformation.apply(spec_with_preconditions) + actual_transformed_spec = transformation.apply(spec_with_preconditions)[0] expected_transformed_spec = FunctionSpecification( preconditions=[], postconditions=[ 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 From 6311651dc540776bae3e683eab47dcb0c860935a Mon Sep 17 00:00:00 2001 From: James Yoo Date: Sun, 22 Feb 2026 16:50:20 -0800 Subject: [PATCH 12/18] Adding scratch work for precondition creation --- .../variants/specification_variant_factory.py | 8 ++- .../variants/transformations/__init__.py | 3 +- .../infer_preconditions_from_ensures.py | 67 +++++++++++++++++++ ...ve_preconditions_to_assigns_and_ensures.py | 10 --- .../transformations/remove_preconditions.py | 12 ---- .../specification_transformation.py | 16 +++-- .../test_infer_preconditions_from_ensures.py | 11 +++ translation/ast/cbmc_ast.py | 13 ++++ 8 files changed, 110 insertions(+), 30 deletions(-) create mode 100644 specifications/variants/transformations/infer_preconditions_from_ensures.py create mode 100644 test/specifications/transformations/test_infer_preconditions_from_ensures.py diff --git a/specifications/variants/specification_variant_factory.py b/specifications/variants/specification_variant_factory.py index bb45af7d..78bbc984 100644 --- a/specifications/variants/specification_variant_factory.py +++ b/specifications/variants/specification_variant_factory.py @@ -2,7 +2,11 @@ from util import FunctionSpecification -from .transformations import MovePreconditionsToAssignsAndEnsures, SpecificationTransformation +from .transformations import ( + MovePreconditionsToAssignsAndEnsures, + RemovePreconditions, + SpecificationTransformation, +) class SpecificationVariantFactory: @@ -18,7 +22,7 @@ class SpecificationVariantFactory: def __init__(self) -> None: """Create a new SpecificationVariantFactory.""" - self._transformations = (MovePreconditionsToAssignsAndEnsures(),) + self._transformations = (MovePreconditionsToAssignsAndEnsures(), RemovePreconditions()) def get_variants(self, spec: FunctionSpecification) -> tuple[FunctionSpecification, ...]: """Return the variants of the given specification. diff --git a/specifications/variants/transformations/__init__.py b/specifications/variants/transformations/__init__.py index 21cd4a7a..4816f94e 100644 --- a/specifications/variants/transformations/__init__.py +++ b/specifications/variants/transformations/__init__.py @@ -1,5 +1,6 @@ from .specification_transformation import SpecificationTransformation from .move_preconditions_to_assigns_and_ensures import MovePreconditionsToAssignsAndEnsures from .remove_preconditions import RemovePreconditions +from .infer_preconditions_from_ensures import InferPreconditionsFromEnsures -__all__ = ["SpecificationTransformation", "MovePreconditionsToAssignsAndEnsures", "RemovePreconditions"] \ No newline at end of file +__all__ = ["SpecificationTransformation", "MovePreconditionsToAssignsAndEnsures", "RemovePreconditions", "InferPreconditionsFromEnsures"] \ No newline at end of file diff --git a/specifications/variants/transformations/infer_preconditions_from_ensures.py b/specifications/variants/transformations/infer_preconditions_from_ensures.py new file mode 100644 index 00000000..2d2d68f1 --- /dev/null +++ b/specifications/variants/transformations/infer_preconditions_from_ensures.py @@ -0,0 +1,67 @@ +"""Transformation for inferring preconditions from expressions in an ensures clause.""" + +from typing import cast + +from translation.ast.cbmc_ast import ( + CBMCAst, + EnsuresClause, + Meta, + Name, + NeqOp, + PtrMemberOp, + RequiresClause, +) +from util import FunctionSpecification + +from .specification_transformation import SpecificationTransformation + + +class InferPreconditionsFromEnsures(SpecificationTransformation): + """TODO: Document me.""" + + def apply(self, specification: FunctionSpecification) -> list[FunctionSpecification]: + """TODO: Document me. + + Args: + specification (FunctionSpecification): _description_ + + Returns: + list[FunctionSpecification]: _description_ + """ + _, postcondition_asts = self._parse_specification(specification) + print(postcondition_asts) + non_null_check_exprs = [ + non_null_check_expr + for ast in postcondition_asts + if (non_null_check_expr := self._get_non_null_check_expr(ast)) + ] + precondition_exprs = [] + for expr in non_null_check_exprs: + match expr: + case NeqOp(lhs, rhs): + non_null_check_subexprs = self._get_non_null_check_subexpressions(lhs) + precondition_exprs = [ + NeqOp(subexpr, rhs) for subexpr in non_null_check_subexprs + ] + case _: + pass + # TODO: How to obtain the appropriate meta... + new_precondition_clauses = [ + RequiresClause(meta=Meta(), expr=expr) for expr in precondition_exprs + ] + print(new_precondition_clauses) + return [] # stub. + + def _get_non_null_check_expr(self, ast: CBMCAst) -> NeqOp | None: + if not isinstance(ast, EnsuresClause): + return None + match ast.expr: + case NeqOp(left=PtrMemberOp(_, _), right=Name("NULL")): + return ast.expr + case _: + return None + + def _get_non_null_check_subexpressions(self, expr: CBMCAst) -> list[CBMCAst]: + if ptr_member_op := cast("PtrMemberOp", expr): + return ptr_member_op.get_dereference_subexpressions() + return [] diff --git a/specifications/variants/transformations/move_preconditions_to_assigns_and_ensures.py b/specifications/variants/transformations/move_preconditions_to_assigns_and_ensures.py index 82ad29c2..f8bc0515 100644 --- a/specifications/variants/transformations/move_preconditions_to_assigns_and_ensures.py +++ b/specifications/variants/transformations/move_preconditions_to_assigns_and_ensures.py @@ -7,9 +7,7 @@ EnsuresClause, OrOp, RequiresClause, - ToAst, ) -from translation.parser import Parser from util import FunctionSpecification from .specification_transformation import SpecificationTransformation @@ -23,14 +21,6 @@ class MovePreconditionsToAssignsAndEnsures(SpecificationTransformation): expressions into conditions for assigns clauses and disjunctions for ensures clauses. """ - def __init__(self) -> None: - """Create a new MovePreconditionsToAssignsAndEnsures.""" - self._parser = Parser( - path_to_grammar_defn="translation/grammar/cbmc.txt", - start="cbmc_clause", - transformer=ToAst(), - ) - def apply(self, specification: FunctionSpecification) -> list[FunctionSpecification]: """Return the result of applying this transformation to the given specification. diff --git a/specifications/variants/transformations/remove_preconditions.py b/specifications/variants/transformations/remove_preconditions.py index fc4be124..958290e2 100644 --- a/specifications/variants/transformations/remove_preconditions.py +++ b/specifications/variants/transformations/remove_preconditions.py @@ -1,9 +1,5 @@ """Transformation where preconditions are removed, one-by-one.""" -from translation.ast.cbmc_ast import ( - ToAst, -) -from translation.parser import Parser from util import FunctionSpecification from .specification_transformation import SpecificationTransformation @@ -12,14 +8,6 @@ class RemovePreconditions(SpecificationTransformation): """Transformation where precondition expressions are removed one-by-one.""" - def __init__(self) -> None: - """Create a new RemovePreconditions.""" - self._parser = Parser( - path_to_grammar_defn="translation/grammar/cbmc.txt", - start="cbmc_clause", - transformer=ToAst(), - ) - def apply(self, specification: FunctionSpecification) -> list[FunctionSpecification]: """Return the result of applying this transformation to the given specification. diff --git a/specifications/variants/transformations/specification_transformation.py b/specifications/variants/transformations/specification_transformation.py index bcde785f..a0b5a959 100644 --- a/specifications/variants/transformations/specification_transformation.py +++ b/specifications/variants/transformations/specification_transformation.py @@ -2,9 +2,7 @@ from abc import ABC, abstractmethod -from translation.ast.cbmc_ast import ( - CBMCAst, -) +from translation.ast.cbmc_ast import CBMCAst, ToAst from translation.parser import Parser from util import FunctionSpecification @@ -18,6 +16,14 @@ class SpecificationTransformation(ABC): _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. @@ -45,6 +51,6 @@ def _parse_specification( specification. """ return ( - [self._parser.parse(clause) for clause in specification.preconditions], - [self._parser.parse(clause) for clause in specification.postconditions], + [self.parser.parse(clause) for clause in specification.preconditions], + [self.parser.parse(clause) for clause in specification.postconditions], ) diff --git a/test/specifications/transformations/test_infer_preconditions_from_ensures.py b/test/specifications/transformations/test_infer_preconditions_from_ensures.py new file mode 100644 index 00000000..27040586 --- /dev/null +++ b/test/specifications/transformations/test_infer_preconditions_from_ensures.py @@ -0,0 +1,11 @@ +from specifications.variants.transformations import InferPreconditionsFromEnsures +from util import FunctionSpecification + +transformation = InferPreconditionsFromEnsures() + +def test_ensures_value_non_null(): + spec_with_non_null_ensures = FunctionSpecification(preconditions=[], postconditions=[ + "__CPROVER_ensures(foo->bar->baz->james != NULL)" + ]) + # TODO: implement me. + diff --git a/translation/ast/cbmc_ast.py b/translation/ast/cbmc_ast.py index ad19cff6..402cc989 100644 --- a/translation/ast/cbmc_ast.py +++ b/translation/ast/cbmc_ast.py @@ -349,6 +349,19 @@ 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] + @dataclass class IndexOp(CBMCAst): From 1b987fd974cd6adb9e14fc868e247ae911071f28 Mon Sep 17 00:00:00 2001 From: James Yoo Date: Mon, 23 Feb 2026 11:16:07 -0800 Subject: [PATCH 13/18] Adding updates to inferring non-null preconditions --- ...fer_non_null_preconditions_from_ensures.py | 77 +++++++++++++++++++ .../infer_preconditions_from_ensures.py | 67 ---------------- ...fer_non_null_preconditions_from_ensures.py | 36 +++++++++ .../test_infer_preconditions_from_ensures.py | 11 --- 4 files changed, 113 insertions(+), 78 deletions(-) create mode 100644 specifications/variants/transformations/infer_non_null_preconditions_from_ensures.py delete mode 100644 specifications/variants/transformations/infer_preconditions_from_ensures.py create mode 100644 test/specifications/transformations/test_infer_non_null_preconditions_from_ensures.py delete mode 100644 test/specifications/transformations/test_infer_preconditions_from_ensures.py 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..e2a1173c --- /dev/null +++ b/specifications/variants/transformations/infer_non_null_preconditions_from_ensures.py @@ -0,0 +1,77 @@ +"""Transformation for inferring non-null preconditions from expressions in an ensures clause.""" + +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): + """TODO: Document me.""" + + def apply(self, specification: FunctionSpecification) -> list[FunctionSpecification]: + """TODO: Document me. + + Args: + specification (FunctionSpecification): _description_ + + Returns: + list[FunctionSpecification]: _description_ + """ + 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: + 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]: + 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/infer_preconditions_from_ensures.py b/specifications/variants/transformations/infer_preconditions_from_ensures.py deleted file mode 100644 index 2d2d68f1..00000000 --- a/specifications/variants/transformations/infer_preconditions_from_ensures.py +++ /dev/null @@ -1,67 +0,0 @@ -"""Transformation for inferring preconditions from expressions in an ensures clause.""" - -from typing import cast - -from translation.ast.cbmc_ast import ( - CBMCAst, - EnsuresClause, - Meta, - Name, - NeqOp, - PtrMemberOp, - RequiresClause, -) -from util import FunctionSpecification - -from .specification_transformation import SpecificationTransformation - - -class InferPreconditionsFromEnsures(SpecificationTransformation): - """TODO: Document me.""" - - def apply(self, specification: FunctionSpecification) -> list[FunctionSpecification]: - """TODO: Document me. - - Args: - specification (FunctionSpecification): _description_ - - Returns: - list[FunctionSpecification]: _description_ - """ - _, postcondition_asts = self._parse_specification(specification) - print(postcondition_asts) - non_null_check_exprs = [ - non_null_check_expr - for ast in postcondition_asts - if (non_null_check_expr := self._get_non_null_check_expr(ast)) - ] - precondition_exprs = [] - for expr in non_null_check_exprs: - match expr: - case NeqOp(lhs, rhs): - non_null_check_subexprs = self._get_non_null_check_subexpressions(lhs) - precondition_exprs = [ - NeqOp(subexpr, rhs) for subexpr in non_null_check_subexprs - ] - case _: - pass - # TODO: How to obtain the appropriate meta... - new_precondition_clauses = [ - RequiresClause(meta=Meta(), expr=expr) for expr in precondition_exprs - ] - print(new_precondition_clauses) - return [] # stub. - - def _get_non_null_check_expr(self, ast: CBMCAst) -> NeqOp | None: - if not isinstance(ast, EnsuresClause): - return None - match ast.expr: - case NeqOp(left=PtrMemberOp(_, _), right=Name("NULL")): - return ast.expr - case _: - return None - - def _get_non_null_check_subexpressions(self, expr: CBMCAst) -> list[CBMCAst]: - if ptr_member_op := cast("PtrMemberOp", expr): - return ptr_member_op.get_dereference_subexpressions() - return [] 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_infer_preconditions_from_ensures.py b/test/specifications/transformations/test_infer_preconditions_from_ensures.py deleted file mode 100644 index 27040586..00000000 --- a/test/specifications/transformations/test_infer_preconditions_from_ensures.py +++ /dev/null @@ -1,11 +0,0 @@ -from specifications.variants.transformations import InferPreconditionsFromEnsures -from util import FunctionSpecification - -transformation = InferPreconditionsFromEnsures() - -def test_ensures_value_non_null(): - spec_with_non_null_ensures = FunctionSpecification(preconditions=[], postconditions=[ - "__CPROVER_ensures(foo->bar->baz->james != NULL)" - ]) - # TODO: implement me. - From 4858d9b51c031ac4234ee554fbb603580646af94 Mon Sep 17 00:00:00 2001 From: James Yoo Date: Mon, 23 Feb 2026 11:21:23 -0800 Subject: [PATCH 14/18] Fixing build errors --- specifications/variants/specification_variant_factory.py | 7 ++++++- specifications/variants/transformations/__init__.py | 4 ++-- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/specifications/variants/specification_variant_factory.py b/specifications/variants/specification_variant_factory.py index 78bbc984..084a254b 100644 --- a/specifications/variants/specification_variant_factory.py +++ b/specifications/variants/specification_variant_factory.py @@ -3,6 +3,7 @@ from util import FunctionSpecification from .transformations import ( + InferNonNullPreconditionsFromEnsures, MovePreconditionsToAssignsAndEnsures, RemovePreconditions, SpecificationTransformation, @@ -22,7 +23,11 @@ class SpecificationVariantFactory: def __init__(self) -> None: """Create a new SpecificationVariantFactory.""" - self._transformations = (MovePreconditionsToAssignsAndEnsures(), RemovePreconditions()) + self._transformations = ( + MovePreconditionsToAssignsAndEnsures(), + RemovePreconditions(), + InferNonNullPreconditionsFromEnsures(), + ) def get_variants(self, spec: FunctionSpecification) -> tuple[FunctionSpecification, ...]: """Return the variants of the given specification. diff --git a/specifications/variants/transformations/__init__.py b/specifications/variants/transformations/__init__.py index 4816f94e..ba6020a6 100644 --- a/specifications/variants/transformations/__init__.py +++ b/specifications/variants/transformations/__init__.py @@ -1,6 +1,6 @@ from .specification_transformation import SpecificationTransformation from .move_preconditions_to_assigns_and_ensures import MovePreconditionsToAssignsAndEnsures from .remove_preconditions import RemovePreconditions -from .infer_preconditions_from_ensures import InferPreconditionsFromEnsures +from .infer_non_null_preconditions_from_ensures import InferNonNullPreconditionsFromEnsures -__all__ = ["SpecificationTransformation", "MovePreconditionsToAssignsAndEnsures", "RemovePreconditions", "InferPreconditionsFromEnsures"] \ No newline at end of file +__all__ = ["SpecificationTransformation", "MovePreconditionsToAssignsAndEnsures", "RemovePreconditions", "InferNonNullPreconditionsFromEnsures"] \ No newline at end of file From aca35e92022858b29a65ae5e671f2bcac3bab8a7 Mon Sep 17 00:00:00 2001 From: James Yoo Date: Mon, 23 Feb 2026 11:33:04 -0800 Subject: [PATCH 15/18] Applying fix --- translation/ast/cbmc_ast.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/translation/ast/cbmc_ast.py b/translation/ast/cbmc_ast.py index 402cc989..871b5eb2 100644 --- a/translation/ast/cbmc_ast.py +++ b/translation/ast/cbmc_ast.py @@ -360,7 +360,7 @@ def get_dereference_subexpressions(self) -> list["PtrMemberOp | CBMCAst"]: """ if isinstance(self.value, PtrMemberOp): return self.value.get_dereference_subexpressions() + [self] - return [self.value] + return [self.value, self] @dataclass From e2d15c12eabf34245b0d861e886b95206b4bf802 Mon Sep 17 00:00:00 2001 From: James Yoo Date: Mon, 23 Feb 2026 12:55:54 -0800 Subject: [PATCH 16/18] Documenting non-null precondition inference transformation --- ...fer_non_null_preconditions_from_ensures.py | 40 ++++++++++++++++--- 1 file changed, 35 insertions(+), 5 deletions(-) diff --git a/specifications/variants/transformations/infer_non_null_preconditions_from_ensures.py b/specifications/variants/transformations/infer_non_null_preconditions_from_ensures.py index e2a1173c..f839b080 100644 --- a/specifications/variants/transformations/infer_non_null_preconditions_from_ensures.py +++ b/specifications/variants/transformations/infer_non_null_preconditions_from_ensures.py @@ -1,4 +1,4 @@ -"""Transformation for inferring non-null preconditions from expressions in an ensures clause.""" +"""Transformation for inferring non-null preconditions from ensures clauses.""" from lark.tree import Meta @@ -17,16 +17,28 @@ class InferNonNullPreconditionsFromEnsures(SpecificationTransformation): - """TODO: Document me.""" + """Transformation for inferring non-null preconditions from ensures clauses.""" def apply(self, specification: FunctionSpecification) -> list[FunctionSpecification]: - """TODO: Document me. + """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): _description_ + specification (FunctionSpecification): The specification to transform. Returns: - list[FunctionSpecification]: _description_ + 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] = [ @@ -54,6 +66,14 @@ def apply(self, specification: FunctionSpecification) -> list[FunctionSpecificat ] 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: @@ -65,6 +85,16 @@ def _get_non_null_check_expr(self, ast: CBMCAst) -> NeqOp | None: 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(_, _): From dac83edc66f25da843d7151e5759a304150f08f6 Mon Sep 17 00:00:00 2001 From: James Yoo Date: Mon, 23 Feb 2026 14:20:02 -0800 Subject: [PATCH 17/18] Starting implementation of minimize conditional assigns --- .../variants/transformations/__init__.py | 3 +- .../minimize_conditional_assigns.py | 96 +++++++++++++++++++ .../test_minimize_conditional_assigns.py | 16 ++++ translation/ast/cbmc_ast.py | 50 +++++++++- 4 files changed, 162 insertions(+), 3 deletions(-) create mode 100644 specifications/variants/transformations/minimize_conditional_assigns.py create mode 100644 test/specifications/transformations/test_minimize_conditional_assigns.py diff --git a/specifications/variants/transformations/__init__.py b/specifications/variants/transformations/__init__.py index ba6020a6..822e7f2a 100644 --- a/specifications/variants/transformations/__init__.py +++ b/specifications/variants/transformations/__init__.py @@ -2,5 +2,6 @@ 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"] \ No newline at end of file +__all__ = ["SpecificationTransformation", "MovePreconditionsToAssignsAndEnsures", "RemovePreconditions", "InferNonNullPreconditionsFromEnsures", "MinimizeConditionalAssigns"] \ No newline at end of file diff --git a/specifications/variants/transformations/minimize_conditional_assigns.py b/specifications/variants/transformations/minimize_conditional_assigns.py new file mode 100644 index 00000000..299d960c --- /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.value) + 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/test/specifications/transformations/test_minimize_conditional_assigns.py b/test/specifications/transformations/test_minimize_conditional_assigns.py new file mode 100644 index 00000000..7073b997 --- /dev/null +++ b/test/specifications/transformations/test_minimize_conditional_assigns.py @@ -0,0 +1,16 @@ +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_assigns(out->target != NULL : out->target)" + ]) + transformed_specs = transformation.apply(spec_with_single_condition_in_assigns) + print(transformed_specs) + assert transformed_specs == [ + FunctionSpecification(preconditions=[], postconditions=[ + "__CPROVER_assigns(out->target)" + ]) + ] diff --git a/translation/ast/cbmc_ast.py b/translation/ast/cbmc_ast.py index 871b5eb2..8c76ade4 100644 --- a/translation/ast/cbmc_ast.py +++ b/translation/ast/cbmc_ast.py @@ -147,7 +147,53 @@ def to_string(self) -> str: @dataclass -class OrOp(BinOp): +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 +class OrOp(LogicalBinOp): left: Any right: Any @@ -159,7 +205,7 @@ def negate(self) -> CBMCAst: @dataclass -class AndOp(BinOp): +class AndOp(LogicalBinOp): left: Any right: Any From 503a4fcf6cdc18b02a78432a8d963a925db3f8f8 Mon Sep 17 00:00:00 2001 From: James Yoo Date: Mon, 23 Feb 2026 14:37:59 -0800 Subject: [PATCH 18/18] Adding test for multiple conditions --- .../transformations/minimize_conditional_assigns.py | 2 +- .../test_minimize_conditional_assigns.py | 11 ++++++++++- 2 files changed, 11 insertions(+), 2 deletions(-) diff --git a/specifications/variants/transformations/minimize_conditional_assigns.py b/specifications/variants/transformations/minimize_conditional_assigns.py index 299d960c..ca7ed0fc 100644 --- a/specifications/variants/transformations/minimize_conditional_assigns.py +++ b/specifications/variants/transformations/minimize_conditional_assigns.py @@ -54,7 +54,7 @@ def apply(self, specification: FunctionSpecification) -> list[FunctionSpecificat 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.value) + new_assigns = Assigns(condition=prefix_condition, targets=assigns_clause.targets) new_postconditions = [*other_postconditions, new_assigns.to_string()] transformed_specs.append( FunctionSpecification( diff --git a/test/specifications/transformations/test_minimize_conditional_assigns.py b/test/specifications/transformations/test_minimize_conditional_assigns.py index 7073b997..1628599d 100644 --- a/test/specifications/transformations/test_minimize_conditional_assigns.py +++ b/test/specifications/transformations/test_minimize_conditional_assigns.py @@ -5,12 +5,21 @@ 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) - print(transformed_specs) 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