Check cfg edge constraints

[Raine-Yang-UofT]

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.)

[coveralls]

Pull Request Test Coverage Report for Build 11109706363

Details

• 19 of 22 (86.36%) changed or added relevant lines in 3 files are covered.
• 1 unchanged line in 1 file lost coverage.
• Overall coverage decreased (-0.02%) to 92.034%

---

Changes Missing Coverage	Covered Lines	Changed/Added Lines	%
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.02%
Covered Lines:	3073
Relevant Lines:	3339

---

💛 - Coveralls

[david-yz-liu]

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]

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]

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]

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")

[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.

[david-yz-liu]

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.

[Raine-Yang-UofT]

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.

[david-yz-liu]

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.