Ordered constraint accumulation #1065
Conversation
| @@ -752,6 +752,102 @@ def test_minimize_02() -> None: | |||
| assert contains_edge(cfg, 8, 6, 40, ('r1', 'r3')) | |||
|
|
|||
|
|
|||
| def test_split_constraint_accumulation() -> None: | |||
| if not maintain_order: | ||
| constraints = sorted(constraints, key=CTerm._constraint_sort_key) |
There was a problem hiding this comment.
IIRC, sorting of constraints was important for the old KSummarizer where we compared nodes for equality a lot. I think it should be fine to just drop sorting without introducing an additional parameter, after testing it on kontrol.
@ehildenb, what do you think?
There was a problem hiding this comment.
Well, I think there are still some places where we could be comparing equality of CTerm without considering different constraint ordering. So I wolud drop the parameter, not sort them by default, and then test with Kontrol. If there are no problems, good to merge. Otherwise, maybe we need to implement explicit equality operator for CTerm directly.
So in short, I agree with @tothtamas28 to not provide the option to have the constraints out of order.
There was a problem hiding this comment.
Great, thank you, I will co-ordinate with @Baltoli and make the changes once the PR has been moved to the new setting of pyk.
Currently,
CSubstconstraints are always sorted when a newCSubstis created. However, when a KCFG is minimized and splits are lifted into other splits, this sorting results in a misordering of constraints and therefore a slightly poorer user experience when trying to debug the control flow. For example, even though the branchings constraints were chronologicallyC1, C2, C3, when the KCFG is minimized they could appear asC2, C3, C1.This PR enables constraint order preservation and uses it when lifting split nodes.