Check cfg edge constraints #1084

Raine-Yang-UofT · 2024-09-21T19:11:27Z

Proposed Changes

Add is_feasible attribute to CFGEdge and implemented update to edge feasibility based on the z3_constraints attribute.
Add handling of AugAssign node in creating edge Z3 constraints.

Existing issue:
The current implementation cannot correctly handle variable reassignment after a conditional statement inside a loop, as shown in the test case test_feasible_reassignment_in_while in test_edge_feasibility

...

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)
🐛 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)	X

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 update_edge_feasibility function that traverses through CFG and checks for logically impossible edges Create unit tests

… check-CFG-edge-constraints

Create test cases for both feasible and unfeasible edges in test_edge_feasibility Add handling of AugAssign node in creating edge Z3 constraints Update change log

…-CFG-edge-constraints

coveralls · 2024-09-21T19:16:29Z

Pull Request Test Coverage Report for Build 11136792286

Warning: This coverage report may be inaccurate.

This pull request's base commit is no longer the HEAD commit of its target branch. This means it includes changes from outside the original pull request, including, potentially, unrelated coverage changes.

For more information on this, see Tracking coverage changes with pull request builds.
To avoid this issue with future PRs, see these Recommended CI Configurations.
For a quick fix, rebase this PR at GitHub. Your next report should be accurate.

Details

22 of 28 (78.57%) changed or added relevant lines in 3 files are covered.
1 unchanged line in 1 file lost coverage.
Overall coverage decreased (-0.09%) to 91.961%

Changes Missing Coverage	Covered Lines	Changed/Added Lines	%
python_ta/cfg/cfg_generator.py	9	12	75.0%
python_ta/cfg/graph.py	12	15	80.0%

Files with Coverage Reduction	New Missed Lines	%
python_ta/cfg/graph.py	1	94.26%

Totals
Change from base Build 11097474413:	-0.09%
Covered Lines:	3077
Relevant Lines:	3346

💛 - Coveralls

david-yz-liu · 2024-09-22T15:19:57Z

python_ta/cfg/graph.py

@@ -274,11 +277,32 @@ def update_edge_z3_constraints(self) -> None:

                # traverse into target node
                for node in edge.target.statements:
-                    if isinstance(node, Assign):


This change should be extracted into a separate pull request. It is separate from checking edge feasibility; it is extending the existing capability of the Z3 constraint updating, which is a good change to make but is separate.

In your new PR, you should make sure to add an entry to the changelog describing this, as well as add new test cases for just this change.

david-yz-liu · 2024-09-22T15:27:13Z

tests/test_cfg/test_edge_feasibility.py

+    )
+
+
+# TODO: determine and implement the expected behavior of this test case


It's okay to not include this test, but please don't include the commented out code in this PR. Instead, save it and include it in a future PR.

david-yz-liu · 2024-09-22T15:29:37Z

python_ta/cfg/graph.py

@@ -3,12 +3,14 @@
 from typing import Any, Dict, Generator, List, Optional, Set

 try:
+    import z3


We should use a consistent import style here. Either import Solver on the line below, or only import z3 and then modify the usages of Z3_OP_UNINTERPRETED to z3.Z3_OP_UNINTERPRETED, etc. consistently throughout.

david-yz-liu · 2024-09-22T15:33:56Z

python_ta/cfg/graph.py

+            for edge in path:
+                solver.add(edge.z3_constraints[path_id])
+                if solver.check() == z3.sat:
+                    edge.is_feasible = True


Overall, I'd like the default value of edge.is_feasible to be True (set in the initializer), and then set to False when the Z3 solver gives "unsatisfiable" for every path that uses the edge.

This is the more conservative default value, in the sense that later on, we'll modify checks to ignore edges that are infeasible, so we want to avoid at all costs the error of marking an edge as infeasible when it's actually feasible.

Your current approach makes the updating a bit awkward because you're iterating across all paths, and then calling solver.check for each path's edge. You should be able to do it the other way, iterating across all edges and then calling solver.check for each edge's set of path constraints. ("if all constraints are unsatisfiable, edge.is_feasible = False")

Set is_feasible to be true by default, and false only if all constrants are unsatisfiable Revert changes to update_edge_z3_constraints

… check-CFG-edge-constraints

david-yz-liu

@Raine-Yang-UofT okay great. I left one minor comment, but also note in my original instructions I asked you to do 3 things. You've done the first two now, and should add the third.

python_ta/cfg/graph.py

Render infeasible CFG edges in light grey Integrate Z3Visitor into CFG rendering

Fix an error that makes edge feasibility when z3 constraints are empty

Update expected snapshot test case for CFG diagram

Create test case without function precondition Refactor certain tests to replace get_paths() to get_edges()

…-Yang-UofT/pyta into check-CFG-edge-constraints

david-yz-liu · 2024-09-30T00:52:59Z

python_ta/cfg/cfg_generator.py

@@ -13,6 +13,8 @@
 from astroid import nodes
 from astroid.builder import AstroidBuilder

+from python_ta.transforms.z3_visitor import Z3Visitor


As with my previous comments, here you should use a relative import (.transforms.z3_visitor) and group this with the imports below.

But also similar to graph.py, we need to check for whether Z3 has been successfully imported or not, and if not then make sure the previous functionality works correctly. You can test this by uninstalling Z3 from your Python environment and then calling generate_cfg.

Hi Professor, I tested that when Z3 is uninstalled, z3_visitor would raise an error as we did not check for Z3 dependency in its imports. I suggest we should modify z3_visitor such that if Z3 dependency is not available, invoking the visitor would do nothing. This may be more convenient than checking for Z3 dependency whenever we want to use Z3Visitor. Should I make this change in a separate PR or include it in this PR.

Hi @Raine-Yang-UofT, please use the approach I described in my original comment. I don't agree with the approach of Z3Visitor "doing nothing" if z3 isn't installed, I'd much rather it not be invoked at all.

@david-yz-liu No problem, I have added a check for z3 dependency in generating CFG. Now the CFG generation works correctly even with Z3 uninstalled. However, as the import of z3 are not checked in Z3Visitor and Z3Parser, we need to fix these two modules for PythonTA to function correctly without Z3. Let me know if I should propose this change in a new PR.

Change the import of Z3Visitor in graph.py to relative import

…-Yang-UofT/pyta into check-CFG-edge-constraints

Invoke Z3Visitor only if z3 is installed

david-yz-liu · 2024-10-02T01:52:49Z

python_ta/cfg/cfg_generator.py

@@ -13,6 +13,7 @@
 from astroid import nodes
 from astroid.builder import AstroidBuilder

+from ..transforms.z3_visitor import Z3Visitor


@Raine-Yang-UofT I'm not sure how you tried to test what I asked for, but transforms.z3_visitor imports z3, and so will raise an ImportError if z3 isn't installed.

Check for import of Z3Visitor in cfg_generator so it works correctly without z3 Implement unit tests for running CFG without z3

Raine-Yang-UofT added 4 commits September 17, 2024 16:20

feat: initially implement update_edge_feasibility

6b77082

Implement update_edge_feasibility function that traverses through CFG and checks for logically impossible edges Create unit tests

Merge branch 'master' of https://github.com/Raine-Yang-UofT/pyta into…

0df453a

… check-CFG-edge-constraints

tests: update unit tests for test_edge_feasibility

820e2a3

Create test cases for both feasible and unfeasible edges in test_edge_feasibility Add handling of AugAssign node in creating edge Z3 constraints Update change log

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

771e419

…-CFG-edge-constraints

docs: fix typo in change log

9f22aba

Raine-Yang-UofT requested a review from david-yz-liu September 21, 2024 19:18

david-yz-liu reviewed Sep 22, 2024

View reviewed changes

Raine-Yang-UofT added 2 commits September 22, 2024 22:13

refactor: reimplement update_edge_feasibility

a4870ed

Set is_feasible to be true by default, and false only if all constrants are unsatisfiable Revert changes to update_edge_z3_constraints

Merge branch 'master' of https://github.com/Raine-Yang-UofT/pyta into…

aa31bda

… check-CFG-edge-constraints

Raine-Yang-UofT requested a review from david-yz-liu September 23, 2024 02:27

david-yz-liu reviewed Sep 24, 2024

View reviewed changes

python_ta/cfg/graph.py Outdated Show resolved Hide resolved

Raine-Yang-UofT added 5 commits September 24, 2024 11:19

refactor: remove unused import

5f1b4d7

docs: resolve change log merge conflict

71c5f1a

feat: implement rendering of infeasible CFG edges

842cff3

Render infeasible CFG edges in light grey Integrate Z3Visitor into CFG rendering

fix: fix incorrect edge feasibility

42a5338

Fix an error that makes edge feasibility when z3 constraints are empty

tests: update testing snapshot

ee18274

Update expected snapshot test case for CFG diagram

Raine-Yang-UofT requested a review from david-yz-liu September 26, 2024 02:53

david-yz-liu and others added 3 commits September 27, 2024 00:50

Merge branch 'master' into check-CFG-edge-constraints

fd5d0ab

test: create unit test with no precondition

2e4ae0f

Create test case without function precondition Refactor certain tests to replace get_paths() to get_edges()

Merge branch 'check-CFG-edge-constraints' of https://github.com/Raine…

b02d72c

…-Yang-UofT/pyta into check-CFG-edge-constraints

david-yz-liu reviewed Sep 30, 2024

View reviewed changes

Raine-Yang-UofT and others added 4 commits September 30, 2024 11:30

Merge branch 'master' into check-CFG-edge-constraints

a090257

refactor: change to relative import

2617624

Change the import of Z3Visitor in graph.py to relative import

chores: resolve merge conflict in change log

99d9fc6

Merge branch 'check-CFG-edge-constraints' of https://github.com/Raine…

b1efa1a

…-Yang-UofT/pyta into check-CFG-edge-constraints

Raine-Yang-UofT requested a review from david-yz-liu September 30, 2024 15:54

fix: check for optional z3 dependency

5b49f71

Invoke Z3Visitor only if z3 is installed

david-yz-liu reviewed Oct 2, 2024

View reviewed changes

fix: allow cfg_generator to work correctly without z3

836bf91

Check for import of Z3Visitor in cfg_generator so it works correctly without z3 Implement unit tests for running CFG without z3

Raine-Yang-UofT requested a review from david-yz-liu October 2, 2024 02:32

david-yz-liu approved these changes Oct 2, 2024

View reviewed changes

david-yz-liu merged commit c7e282b into pyta-uoft:master Oct 2, 2024
15 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Check cfg edge constraints #1084

Check cfg edge constraints #1084

Raine-Yang-UofT commented Sep 21, 2024 •

edited

Loading

coveralls commented Sep 21, 2024 •

edited

Loading

david-yz-liu Sep 22, 2024

david-yz-liu Sep 22, 2024

david-yz-liu Sep 22, 2024

david-yz-liu Sep 22, 2024

david-yz-liu left a comment

david-yz-liu Sep 30, 2024

Raine-Yang-UofT Sep 30, 2024

david-yz-liu Sep 30, 2024

Raine-Yang-UofT Sep 30, 2024

david-yz-liu Oct 2, 2024

		)


		# TODO: determine and implement the expected behavior of this test case

Check cfg edge constraints #1084

Check cfg edge constraints #1084

Conversation

Raine-Yang-UofT commented Sep 21, 2024 • edited Loading

Proposed Changes

Type of Change

Checklist

Questions and Comments

coveralls commented Sep 21, 2024 • edited Loading

Pull Request Test Coverage Report for Build 11136792286

Warning: This coverage report may be inaccurate.

Details

💛 - Coveralls

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

Raine-Yang-UofT commented Sep 21, 2024 •

edited

Loading

coveralls commented Sep 21, 2024 •

edited

Loading