Skip to content

Type Equality/Compatibility Revamp #286

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 8 commits into from
Jun 11, 2024
Merged

Type Equality/Compatibility Revamp #286

merged 8 commits into from
Jun 11, 2024

Conversation

lwaern-intel
Copy link
Contributor

Taken from #213, but with some refinements

Gonna run this against VP once verification passes. I'm 50/50 on whether it causes breakage. On one hand, this definitely tightens down the equality logic. On the other hand, GCC should have been rejecting the cases that slips through, unless some warnings get disabled or something.

@lwaern-intel lwaern-intel requested a review from mandolaerik May 27, 2024 06:48
return 0
if self.base.cmp(other.base) == 0:
return 0
return NotImplemented
Copy link
Contributor Author

@lwaern-intel lwaern-intel May 27, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is a strange one. Previously, TArray.cmp 's logic caused it to be more lenient without the dml12_misc compatibility feature. I originally thought that maybe you made a mistake while making #209, but no, that was true even before then. Same story with TPtr.cmp.
While moving old behaviors of cmp to cmp_fuzzy I've just dropped these dml12_misc checks of TArray and TPtr.

@lwaern-intel
Copy link
Contributor Author

Oh, we even have an issue about this: SIMICS-9504. I wouldn't say this closes completely closes (just contributes to fixing it) , due to this still hanging onto cmp_fuzzy as a HACK for some of the cases that SIMICS-9504 touches upon. The primary point of this PR is to introduce a mechanism for strict type equality (which we can leverage for e.g. idempotent externs), and secondarily to convert most aspects of DMLC to leverage that mechanism. The remaining parts that still uses cmp_fuzzy constitute the most difficult cases, where some kind of type unification or conversion are needed (such as the ternary operator and comparison operators.)

@syssimics
Copy link
Contributor

Verification #13419451: ❌ fail

py/dml/ctree.py Outdated
raise ECAST(site, expr, new_type)
if isinstance(real, (TVoid, TArray, TVector, TTraitList, TFunction)):
if old_type.cmp(real) == 0:
Copy link
Contributor Author

@lwaern-intel lwaern-intel May 27, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I just realized this path is disgustingly not always correct due to bitfields. A 64-bit bitfields is completely type compatible with uint64, even in the sense as laid out by the docstring of DMLType.cmp, and yet DMLC will treat them differently w.r.t. mkSubRef, so just spitting out the same expression mkRValue-d is not correct. I suppose we could have an ad-hoc exception for those cases.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Alternatively, instead of doing mkRValue, add an arg for Cast that tells it not to spit out a cast in generated C. Or an alternate class to Cast that does the same thing. Or use Cast anyway.

Copy link
Contributor Author

@lwaern-intel lwaern-intel May 27, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This also really highlights the difference between type equality and type compatibility. We've gotten away with treating them as one and the same, but in this instance that falls apart. Does that mean we should introduce a separate mechanism for type equality...?

Copy link
Contributor Author

@lwaern-intel lwaern-intel May 27, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we'll be forced to, unless we're willing to treat bitfields as type-incompatible with the corresponding uintX type. Consider idempotent externs; an extern with a bitfields arg can be called using {} initializer syntax for the argument, but an extern with a uintX arg cannot. We cannot consider two declarations differing in that aspect equal to one another, even though their signatures are completely compatible. There's a similar issue with method declarations and overrides.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The notion of type equality would thus be type compatibility with an additional restriction: that DMLC treats the type identically in all ways that are visible to the modeler.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Added an ad-hoc exception for the moment.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think compatibility between uintN and bitfields N is important -- one can surely come up with use cases, but I can't see how they would be common (e.g., did you ever get a uint64 pointer that you want to pass to a function that takes a bitfields pointer?). If making them incompatible removes the need for a "type equality" concept, then it's most likely worth it. Especially since we now have a compat feature to hijack.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If it's easy to introduce uintN vs bitfeldsN incompatibility separately, without the full type revamp, then it would be nice to run that with jenkins, to grasp how much this part would break.

Copy link
Contributor Author

@lwaern-intel lwaern-intel May 29, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

hah my ad-hoc exception wasn't good enough to clear jenkins:

        vid1 = (cast(&vid1, vlan_tag_t *))->vid;

&vid is uint16 * which is considered compatible with vlan_tag_t * and thus mkRValue is used, oops.

Anyhoo, I'll try out adding a rule that a bitfields is only considered compatible to another bitfields if they share the same exact members (maybe with some memoization...?) in addition to the other properties like signedness and endianness.

@syssimics
Copy link
Contributor

Verification #13420028: ❌ fail

@lwaern-intel lwaern-intel force-pushed the lw/typeeq-revamp branch 4 times, most recently from b84631b to b4c81c9 Compare May 27, 2024 10:47
@lwaern-intel lwaern-intel marked this pull request as draft May 27, 2024 10:49
@lwaern-intel
Copy link
Contributor Author

making this draft as I'm discovering there's needed stuff in the RAII pr I forgot to break out. Will make this non-draft when verification passes in the compatibility PR

@lwaern-intel lwaern-intel marked this pull request as ready for review May 29, 2024 09:58
@lwaern-intel
Copy link
Contributor Author

lwaern-intel commented May 29, 2024

This does break VP violently, unfortunately. A compatibility feature has been added to gate the aspects that cause breakage.

if safe_realtype(mt).cmp(
safe_realtype(func_type.output_type)) != 0:
if safe_realtype_unconst(mt).cmp(
safe_realtype_unconst(func_type.output_type)) != 0:
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Did not gate these behind the compatibility feature. Did not seen any new error message from them. Will confirm with a rerun, though.

@syssimics
Copy link
Contributor

Verification #13432053: ✅ pass

@syssimics
Copy link
Contributor

Verification #13435945: ✅ pass

@lwaern-intel lwaern-intel force-pushed the lw/typeeq-revamp branch 2 times, most recently from c513228 to 315bbec Compare June 10, 2024 16:47
typ_clone.const = True
self.assertFalse(typ.const)
typ = typ_clone.clone()
self.assertTrue(typ.const)
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Note this addition to the clone test. This catches the previously bad TVoid and TBool implementations.

@lwaern-intel lwaern-intel requested a review from mandolaerik June 10, 2024 17:02
@syssimics
Copy link
Contributor

Verification #13481859: ✅ pass

* a.eq(b) must imply a.key() == b.key()
* a.key() == b.key() implies a.eq(b) with overwhelming likelihood
(though not necessarily guaranteed; see IntegerType.key())
'''
Copy link
Contributor Author

@lwaern-intel lwaern-intel Jun 11, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The changes to key() in this PR technically causes backwards checkpoint incompatibility... were it not for the fact that key() is currently only used for hook.send_now() callbacks of afters. Making it completely irrelevant in practice.

@syssimics
Copy link
Contributor

Verification #13483956: ✅ pass

@lwaern-intel lwaern-intel requested a review from mandolaerik June 11, 2024 10:15
@syssimics
Copy link
Contributor

Verification #13485192: ✅ pass

@syssimics
Copy link
Contributor

Verification #13485399: ✅ pass

@lwaern-intel
Copy link
Contributor Author

@lwaern-intel lwaern-intel merged commit b2c6d68 into main Jun 11, 2024
2 checks passed
@lwaern-intel lwaern-intel deleted the lw/typeeq-revamp branch June 14, 2024 12:32
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants