Fix Loop Handling and Reporting Issues in Z3 Constraints and one-iteration-checker
#1116
Conversation
Implement z3 option for one_iteration_checker Create unit tests
Check whether the loop has at least one iteration by z3 constraints
Implement a test case that fails the current implementation
Add cycles to paths during CFG path traverse Update unit tests
Fix an error in one-iteration-checker that causes error message not correctly reported for while loops
Pull Request Test Coverage Report for Build 12076085936Warning: 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.
Details
💛 - Coveralls |
python_ta/cfg/graph.py
Outdated
| if ( | ||
| current_edge.target == self.end | ||
| or current_edge.target in visited_nodes | ||
| or all(edge in visited_edges for edge in current_edge.target.successors) |
There was a problem hiding this comment.
this can be simplified into a set subset operation
| expected_while_true_path = [ | ||
| {x > 5, y > 10}, | ||
| {x > 5, y > 10, x + y > 15}, | ||
| {}, |
There was a problem hiding this comment.
It seems quite strange for this to be here. What edge is this supposed to correspond to?
All edges should, at a minimum, have the precondition constraints. So if you're getting an empty set something seems off. (Note: {} is an empty dict literal, which is even more suspicious.)
There was a problem hiding this comment.
Hi Professor, I think this is the expected behavior. This edge corresponds to the highlighted one pointing from loop body to condition. Since both x and y are reassigned in the loop body, all z3 constraints that involves x and y, including precondition, are removed.
There was a problem hiding this comment.
Okay that makes sense, thanks. The value is fine, but see my other comment about {} not being the appropriate data type. It's strange that the tests didn't pick up on that, you should investigate why not.
There was a problem hiding this comment.
Hi Professor, thanks for the reminder. Even though we do expect an empty set here, but {} is an empty dictionary. I will definitely look into what's going on here.
There was a problem hiding this comment.
Hi Professor, I’ve changed the empty dictionary to set(). The reason the tests passed previously is that they iterate through and compare each z3 constraint using zip(actual, expected). When the collection is empty—whether it’s a set or a dictionary—this iteration doesn’t execute. This behavior shouldn’t cause any issues since we’ve already verified that the lengths of expected and actual are equal beforehand.
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.)
...
Screenshots of your changes (if applicable)
Type of Change
(Write an
Xor a brief description next to the type or types that best describe your changes.)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:
After opening your pull request:
Questions and Comments
(Include any questions or comments you have regarding your changes.)