Refactor to_dict method in EpsilonStatus class #163
Conversation
Auto-verify is providing obtained_labels as a string, not a numpy array or list, but we called .flatten() (a numpy array method). The to_dict() method assumes obtained_labels is always a numpy array, but it's actually receiving different types. Proposed fix: Update the to_dict() method in epsilon_status.py to handle multiple types robustly:
… the counter example and populate obtained_labels in the CompleteVerificationData
henba1
changed the title
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
…sult in auto_verify_module verify() with tests
Aaron99B
left a comment
Aaron99B
left a comment
There was a problem hiding this comment.
I wouldn't include short inline comments if not absolutely necessary. The code should be self-explanatory. If we include many of these comments, we will have to update even more things if we make any changes.
| """Convert the EpsilonStatus to a dictionary.""" | ||
| obtained_labels_value = None | ||
| if self.obtained_labels is not None: | ||
| if hasattr(self.obtained_labels, "flatten"): # numpy array |
There was a problem hiding this comment.
Let's just check for a numpy array here. Then we can also remove the comment that it is a numpy array
| obtained_labels_value = self.obtained_labels.flatten().tolist() | ||
| elif isinstance(self.obtained_labels, list): | ||
| obtained_labels_value = self.obtained_labels | ||
| else: # string or other type |
There was a problem hiding this comment.
I would not include comments like this. The code itself should be readable enough
| obtained_labels_value = self.obtained_labels.flatten().tolist() | ||
| elif isinstance(self.obtained_labels, list): | ||
| obtained_labels_value = self.obtained_labels | ||
| else: # string or other type |
There was a problem hiding this comment.
How could we reach this else case? Right now it could just be numpy array or list, right?
There was a problem hiding this comment.
obtained_labels is expected to be either a numpy array or a list, but we can keep the else branch as a safe fallback to handle scalar values (e.g. a single string), which is covered by the unit test test_epsilon_status l. 98-109
This would enable obained_labels also to be str - it just extends and does not break anything.
| self.timeout = timeout | ||
| self.config = config | ||
| self.name = f"AutoVerifyModule ({verifier.name})" | ||
| self.name = f"AutoVerifyModule ({verifier.name})" |
There was a problem hiding this comment.
No functional changes, the formatting of the verify_property call was changed (arguments on one line vs multiple lines)
There was a problem hiding this comment.
If you mean only this line, then its likely some artefact - ie blank space removed
There was a problem hiding this comment.
Addressed - only formatting changes
|
|
||
| assert isinstance(result, CompleteVerificationData) | ||
| assert result.result == "SAT" | ||
| # obtained_labels should not be set if parsing fails |
There was a problem hiding this comment.
Why don't you assert it then?
| # obtained_labels should not be set if parsing fails | ||
|
|
||
|
|
||
| def test_auto_verify_module_verify_error_result(auto_verify_module, verification_context): |
There was a problem hiding this comment.
What funtionality is tested here? Is this test really necessary?
There was a problem hiding this comment.
error handling path when the verifier returns an Err result
I think we should keep it as we want explicit coverage of the error path
Auto-verify is providing obtained_labels as a string, not a numpy array or list, but we called .flatten() (a numpy array method).
The to_dict() method assumes obtained_labels is always a numpy array, but it's actually receiving different types.
Proposed fix: Update the to_dict() method in epsilon_status.py to handle multiple types robustly: