Condition Logic Checker #1114

Raine-Yang-UofT · 2024-11-15T20:02:54Z

Proposed Changes

(Describe your changes here. Also describe the motivation for your changes: what problem do they solve, or how do they improve the application or codebase? If this pull request fixes an open issue, use a keyword to link this pull request to the issue.)

Implement a custom checker for the following messages:

redundant-condition: a conditional statement is guaranteed true given the control flow leading to the statement.
impossible-condition: a conditional statement is guaranteed false either due to contradition within the statement or contradiction with conditions leading to the statement.

These two messages are enabled only if Z3 dependency is installed and z3 option is turned on for PythonTA

Additional changes:
In check-examples, the z3 option is set to True to check for redundant-condition and impossible-condition

...

Screenshots of your changes (if applicable)

Type of Change

(Write an X or a brief description next to the type or types that best describe your changes.)

Type	Applies?
🚨 Breaking change (fix or feature that would cause existing functionality to change)
✨ New feature (non-breaking change that adds functionality)	X
🐛 Bug fix (non-breaking change that fixes an issue)
♻️ Refactoring (internal change to codebase, without changing functionality)
🚦 Test update (change that only adds or modifies tests)
📚 Documentation update (change that only updates documentation)
📦 Dependency update (change that updates a dependency)
🔧 Internal (change that only affects developers or continuous integration)

Checklist

(Complete each of the following items for your pull request. Indicate that you have completed an item by changing the [ ] into a [x] in the raw text, or by clicking on the checkbox in the rendered description on GitHub.)

Before opening your pull request:

I have performed a self-review of my changes.
- Check that all changed files included in this pull request are intentional changes.
- Check that all changes are relevant to the purpose of this pull request, as described above.
I have added tests for my changes, if applicable.
- This is required for all bug fixes and new features.
I have updated the project documentation, if applicable.
- This is required for new features.
I have updated the project Changelog (this is required for all changes).
If this is my first contribution, I have added myself to the list of contributors.

After opening your pull request:

I have verified that the pre-commit.ci checks have passed.
I have verified that the CI tests have passed.
I have reviewed the test coverage changes reported by Coveralls.
I have requested a review from a project maintainer.

Questions and Comments

(Include any questions or comments you have regarding your changes.)

Implement feature for redundant_condition_checker Refactor z3 constraints traverse in CFG module Create unit tests for redundant_condition_checker

Implement checker for impossible condition Refactor checker for redundant condition Add more unit tests for redundant and impossible condition Create examples for redundant and impossible condition

Fix an error that unregisters checker during initialization Add examples for redundant and impossible conditions Fix an unit test's expected behavior Update checker documentation Modify check-examplet to take z3 argument

modify ControlFlowGraph to append node z3_constraint only when it's not none Enable z3 option in test_examples

Initialize z3_constraint attribute of CFGBlock with None Turn on z3 option for test_black and test_check

coveralls · 2024-11-18T07:15:49Z

Pull Request Test Coverage Report for Build 12405548908

Details

45 of 50 (90.0%) changed or added relevant lines in 3 files are covered.
No unchanged relevant lines lost coverage.
Overall coverage increased (+0.02%) to 91.881%

Changes Missing Coverage	Covered Lines	Changed/Added Lines	%
python_ta/patches/transforms.py	2	3	66.67%
python_ta/checkers/condition_logic_checker.py	39	43	90.7%

Totals
Change from base Build 12248278358:	0.02%
Covered Lines:	3146
Relevant Lines:	3424

💛 - Coveralls

Revert changes to transforms, test_black, and test_examples

examples/custom_checkers/r9900_redundant_condition.py

examples/custom_checkers/r9901_impossible_condition.py

python_ta/checkers/redundant_or_impossible_condition_checker.py

david-yz-liu · 2024-11-22T02:41:17Z

python_ta/checkers/redundant_or_impossible_condition_checker.py

+        if not node_block.is_feasible or node_block.z3_constraint is None:
+            return
+
+        for pred in node_block.predecessors:


only include feasible edges here; this also removes the need for a node_block.is_feasible check above, as if there are no feasible predecessor edges the loop won't run at all

python_ta/cfg/graph.py

david-yz-liu · 2024-11-22T02:51:59Z

python_ta/checkers/redundant_or_impossible_condition_checker.py

+
+        node_block = node.cfg_block
+
+        if not node_block.is_feasible or node_block.z3_constraint is None:


Rather than create a separate instance attribute z3_constraint:

Extract the condition of the node object

Create a new Z3Environment from the variables from the underlying CFG (you can define a new ControlFlowGraph to produce this environment).

Use the environment to parse the condition expression directly, in this function.

Hi Professor, I'm still working on this part and am unsure how to proceed. The main issue is that I cannot determine how to access the ControlFlowGraph instance associated with a node. Currently, I can only access the node's CFGBlock, which does not contain a reference back to the ControlFlowGraph.

My previous approach of adding z3_constraint to nodes could be the most convenient implementation. I understand your design decision to avoid embedding too much information directly into the control flow graph itself. However, even if I find a way to access the ControlFlowGraph, we would still need a mechanism to track the reassignment status of variables within the current block, as this is not currently handled by the CFG.

In summary, I’m currently unable to parse the condition effectively without modifying the graph.py module. I’d appreciate any suggestions you might have on how to proceed without altering the core module or if adjustments to it might be acceptable.

@Raine-Yang-UofT this is a good summary of your current understanding. You said:

The main issue is that I cannot determine how to access the ControlFlowGraph instance associated with a node. Currently, I can only access the node's CFGBlock, which does not contain a reference back to the ControlFlowGraph.

Every astroid node can access its enclosing frame (either a function definition or the Module), I think the method is called .frame() or something similar. From this you can access the enclosing CFG.

@david-yz-liu Hi Professor, thanks for this hint. However, there is another tricky problem even after accessing ControlFlowGraph - knowing the reassignment status of each variables.

In our implementation, we discard the variables being reassigned in subsequent z3 constraints. As a result, to correctly parse the node condition, we need not only the z3 variables provided by ControlFlowGraph, but also which variables are reassigned when we reach the condition node, information we do not have even with ControlFlowGraph.

In addition, as the variable reassignment status may be different along different execution paths, it is possible that on different execution paths the node condition constraints should be parsed differently.

Given these problems, the most convenient solution might be adding z3_constraints to CFGBlock during graph traverse, where we have all the information above. Let me know how should I proceed.

Hi @Raine-Yang-UofT, whether or not variables are reassigned should impact the constraints stored in the edges, but this should not impact the conversion of the if/while condition.

The algorithm used by these checkers should always use the translated if/while condition. The reassignments will impact how this condition is combined with the existing path constraints that reach the condition.

Add additional comments to checker examples Add unit test for redundant-condition-checker

Rename checker to ConditionLogicChecker Add example case for redundant condition

Use single _check_unsat to handle both redundant condition and impossible condition Revert changes to transforms

…dant-or-impossible-condition-checker

Use Z3Environment of CFG variables to parse node condition Change z3_var attribute of ControlFlowGraph to public

Change condition of redundant/impossible condition to to be triggered only if the z3 check fails for all branches for all paths Add test cases for multiple feasible branches

Turn on `separate-condition-block` in CFGVisitor when `z3` config applied Update unit tests

david-yz-liu

@Raine-Yang-UofT great work! I left a few inline comments, which should be pretty small.

I did note one oddity: both the redundant and impossible condition checks were being triggered on my top-level if __name__ == '__main__' condition, even when they shouldn't have been. I'm not sure exactly why this is, can you please look into it?

david-yz-liu · 2024-12-18T22:36:20Z

CHANGELOG.md

@@ -43,6 +43,8 @@ and adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 ### 💫 New checkers

 - `unmentioned-parameter`: Provide error message when a function parameter is not mentioned by name in the function's docstring. By default, this checker is disabled.
+- `redundant-condition`: Provide error message when a conditional statement within a function is guaranteed true. This checker requires `z3` option to be turned on.


These should be moved into the unreleased section (note that I made a version update recently, so this part of the changelog now refers to 2.9.0).

david-yz-liu · 2024-12-18T22:37:47Z

docs/checkers/index.md

+
+```
+
+This error will only be checked if `z3` dependency is install and `z3` option of PythonTA


z3 dependency -> the z3-solver library

install -> installed

is turned on -> is enabled

david-yz-liu · 2024-12-18T22:37:56Z

docs/checkers/index.md

+
+```
+
+This error will only be checked if `z3` dependency is install and `z3` option of PythonTA


similar to above

david-yz-liu · 2024-12-18T22:38:38Z

examples/custom_checkers/r9900_redundant_condition.py

+    return 0
+
+
+def redundant_condition(x: bool):


include a return type annotation of None here

david-yz-liu · 2024-12-18T22:38:55Z

examples/custom_checkers/r9901_impossible_condition.py

@@ -0,0 +1,28 @@
+def print_none_negative_number(x: int):


include a return type annotation

david-yz-liu · 2024-12-18T22:47:40Z

python_ta/checkers/condition_logic_checker.py

+            self.add_message("impossible-condition", node=node)
+
+    def _check_unsat(self, prev_constraints: z3.ExprRef, node_constraint: z3.ExprRef) -> bool:
+        """Check if the condition is redundant."""


This docstring isn't quite right. This function returns whether the And of its two inputs is unsatisfiable.

david-yz-liu · 2024-12-18T22:49:54Z

tests/test_examples.py

@@ -149,7 +150,7 @@ def test_examples_files_pyta(test_file: str, pyta_examples_symbols: dict[str, se
    found_pylint_message = checker_name in file_symbols
    assert (
        found_pylint_message
-    ), f"Failed {test_file}. File does not add expected message  {file_symbols}."
+    ), f"Failed {test_file}. File does not add expected message {checker_name}:  {file_symbols}."


This change is okay, but please delete the extra space after the colon

david-yz-liu · 2024-12-18T22:53:13Z

python_ta/checkers/condition_logic_checker.py

+            for edge in (pred for pred in node_block.predecessors if pred.is_feasible)
+            for constraints in edge.z3_constraints.values()
+        ):
+            self.add_message("redundant-condition", node=node)


pass node.test as the argument (so that only the condition is highlighted)

david-yz-liu · 2024-12-18T22:53:19Z

python_ta/checkers/condition_logic_checker.py

+            for edge in (pred for pred in node_block.predecessors if pred.is_feasible)
+            for constraints in edge.z3_constraints.values()
+        ):
+            self.add_message("impossible-condition", node=node)


same as above

david-yz-liu · 2024-12-18T22:54:48Z

python_ta/checkers/condition_logic_checker.py

+"""
+Check for redundant If or While conditions in functions based on z3 constraints
+"""
+


Include a from __future__ import annotations, otherwise the type annotation z3.ExprRef below will raise an error if z3 is not installed

Modify comments and error messages Add type annotations to example code Change node.test to be the node highlighted Update unit tests

Add checking for condition z3 expression to be not-None Add test cases for None condition

david-yz-liu

Thank you for all of your work on this, @Raine-Yang-UofT!

Raine-Yang-UofT added 3 commits November 8, 2024 00:26

feat: implement basic checker feature

e30f7fa

Implement feature for redundant_condition_checker Refactor z3 constraints traverse in CFG module Create unit tests for redundant_condition_checker

feat: implement impossible-condition-checker

0f173f6

Implement checker for impossible condition Refactor checker for redundant condition Add more unit tests for redundant and impossible condition Create examples for redundant and impossible condition

fix: register checker to linter & add documentation

a9b24f6

Fix an error that unregisters checker during initialization Add examples for redundant and impossible conditions Fix an unit test's expected behavior Update checker documentation Modify check-examplet to take z3 argument

Raine-Yang-UofT requested a review from david-yz-liu November 15, 2024 20:03

Raine-Yang-UofT added 6 commits November 15, 2024 16:04

fix: fix typo in documentation

7bc4b7c

fix: fix type annotation for compatibility with older Python version

a43c5bf

ci: remove z3 option to rerun CI tests

b53c450

fix: add node z3_constraint only if constraint is not none

613e81a

modify ControlFlowGraph to append node z3_constraint only when it's not none Enable z3 option in test_examples

tests: add docstrings in example test cases

65be1ed

fix: fix failing unit tests

4be4558

Initialize z3_constraint attribute of CFGBlock with None Turn on z3 option for test_black and test_check

refactor: revert changes

6593e85

Revert changes to transforms, test_black, and test_examples

david-yz-liu reviewed Nov 22, 2024

View reviewed changes

Raine-Yang-UofT added 3 commits November 22, 2024 01:47

docs: update examples

1d73c95

Add additional comments to checker examples Add unit test for redundant-condition-checker

refactor: rename checker

10076c9

Rename checker to ConditionLogicChecker Add example case for redundant condition

refactor: rename checker and remove outdated comments

fbca50e

Raine-Yang-UofT changed the title ~~Redundant or impossible condition checker~~ Condition logic checker Nov 26, 2024

Raine-Yang-UofT changed the title ~~Condition logic checker~~ Condition Logic Checker Nov 26, 2024

Raine-Yang-UofT added 5 commits November 26, 2024 16:53

refactor: revert changes to graph.py

54ad929

refactor: remove redundant helper function

5ab960b

Use single _check_unsat to handle both redundant condition and impossible condition Revert changes to transforms

docs: refine examples

76aeafc

fix: revert file path changes to test_exampes

ec386e9

Merge branch 'master' of https://github.com/pyta-uoft/pyta into redun…

68f736d

…dant-or-impossible-condition-checker

Raine-Yang-UofT requested a review from david-yz-liu November 28, 2024 22:36

Raine-Yang-UofT added 5 commits November 28, 2024 17:41

docs: refine documentation

78d4d2d

refactor: use Z3Environment to parse node condition

950e18a

Use Z3Environment of CFG variables to parse node condition Change z3_var attribute of ControlFlowGraph to public

fix: fix failing test when multiple feasible branches are present

ce10717

Change condition of redundant/impossible condition to to be triggered only if the z3 check fails for all branches for all paths Add test cases for multiple feasible branches

fix: fix condition logic error not ignored during reassignment

a33367e

Turn on `separate-condition-block` in CFGVisitor when `z3` config applied Update unit tests

fix: resolve merge conflicts

e7a102c

david-yz-liu reviewed Dec 18, 2024

View reviewed changes

Raine-Yang-UofT added 2 commits December 18, 2024 21:48

refactor: refine comments and documentation

96aa91d

Modify comments and error messages Add type annotations to example code Change node.test to be the node highlighted Update unit tests

fix: fix false error reporting when condition is None

1e0a29e

Add checking for condition z3 expression to be not-None Add test cases for None condition

Raine-Yang-UofT requested a review from david-yz-liu December 19, 2024 03:25

david-yz-liu approved these changes Dec 19, 2024

View reviewed changes

david-yz-liu merged commit c1f4019 into pyta-uoft:master Dec 19, 2024
15 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Condition Logic Checker #1114

Condition Logic Checker #1114

Raine-Yang-UofT commented Nov 15, 2024 •

edited

Loading

coveralls commented Nov 18, 2024 •

edited

Loading

david-yz-liu Nov 22, 2024

david-yz-liu Nov 22, 2024

Raine-Yang-UofT Nov 28, 2024 •

edited

Loading

david-yz-liu Nov 29, 2024

Raine-Yang-UofT Nov 30, 2024

david-yz-liu Nov 30, 2024

david-yz-liu left a comment

david-yz-liu Dec 18, 2024

david-yz-liu Dec 18, 2024

david-yz-liu Dec 18, 2024

david-yz-liu Dec 18, 2024

david-yz-liu Dec 18, 2024

david-yz-liu Dec 18, 2024

david-yz-liu Dec 18, 2024

david-yz-liu Dec 18, 2024

david-yz-liu Dec 18, 2024

david-yz-liu Dec 18, 2024

david-yz-liu left a comment


		node_block = node.cfg_block

		if not node_block.is_feasible or node_block.z3_constraint is None:


		```

		This error will only be checked if `z3` dependency is install and `z3` option of PythonTA

Condition Logic Checker #1114

Condition Logic Checker #1114

Conversation

Raine-Yang-UofT commented Nov 15, 2024 • edited Loading

Proposed Changes

Type of Change

Checklist

Questions and Comments

coveralls commented Nov 18, 2024 • edited Loading

Pull Request Test Coverage Report for Build 12405548908

Details

💛 - Coveralls

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Raine-Yang-UofT Nov 28, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

david-yz-liu left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

david-yz-liu left a comment

Choose a reason for hiding this comment

Raine-Yang-UofT commented Nov 15, 2024 •

edited

Loading

coveralls commented Nov 18, 2024 •

edited

Loading

Raine-Yang-UofT Nov 28, 2024 •

edited

Loading