Skip to content
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

veri: disallow duplicate specs #87

Merged
merged 2 commits into from
Jan 31, 2024
Merged

Conversation

mmcloughlin
Copy link
Collaborator

This PR errors when duplicate specs are provided.

We currently have two for lower_icmp_const:

(spec (lower_icmp_const c x y in_ty)

(spec (lower_icmp_const c x y in_ty)

@@ -4567,35 +4567,6 @@
(if (ty_int_ref_scalar_64 ty))
(flags_and_cc (cmp (operand_size ty) rn rm) cond))

(spec (lower_icmp_const c x y in_ty)
Copy link
Collaborator Author

Choose a reason for hiding this comment

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

@avanhatt Which of the specs should be kept?

Copy link
Owner

Choose a reason for hiding this comment

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

On first glance, they look equivalent, but the one with the specific enum names (the one deleted here) is a little cleaner to read IMO. Let's keep this one instead.

@mmcloughlin mmcloughlin requested a review from avanhatt November 28, 2023 01:57
@mmcloughlin mmcloughlin marked this pull request as ready for review November 28, 2023 01:57
@@ -4567,35 +4567,6 @@
(if (ty_int_ref_scalar_64 ty))
(flags_and_cc (cmp (operand_size ty) rn rm) cond))

(spec (lower_icmp_const c x y in_ty)
Copy link
Owner

Choose a reason for hiding this comment

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

On first glance, they look equivalent, but the one with the specific enum names (the one deleted here) is a little cleaner to read IMO. Let's keep this one instead.

@mmcloughlin mmcloughlin force-pushed the mbm/disallow-dupe-specs branch from 4ec32ef to 514bf33 Compare November 29, 2023 16:12
@mmcloughlin mmcloughlin requested a review from avanhatt November 29, 2023 19:05
@mmcloughlin mmcloughlin force-pushed the mbm/disallow-dupe-specs branch from 514bf33 to 287d3f7 Compare January 31, 2024 22:40
@mmcloughlin mmcloughlin merged commit e080095 into verify-main Jan 31, 2024
2 checks passed
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this pull request Oct 9, 2024
Now we have the `(with ...)` scope there is no need to use unique
`v<i>_<j>` prefixes for temporary variables. This PR switches to use
`t<i>` names.

Aside from looking nicer it also removes a piece of config we need to
track.

Updates avanhatt#62
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.

2 participants