Skip to content

Add support for f16 and f128 for toolchain upgrade to 6/28 - #3306

Merged
adpaco merged 17 commits into
model-checking:mainfrom
jaisnan:toolchain-upgrade-3303
Jul 1, 2024
Merged

Add support for f16 and f128 for toolchain upgrade to 6/28#3306
adpaco merged 17 commits into
model-checking:mainfrom
jaisnan:toolchain-upgrade-3303

Conversation

@jaisnan

@jaisnanjaisnan commented Jun 28, 2024•
edited
Loading

Copy link
Copy Markdown
Contributor

Adds support for f16 and f128, i.e

  1. adding translation to irep .
  2. generating arbitrary values for the new types
  3. generating basic invariants (checking if safe) for new types
  4. Adds sanity testing for arbitrary on the new types.

Resolves#3303

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@jaisnan
jaisnan requested a review from a team as a code ownerJune 28, 2024 16:22
@github-actionsgithub-actionsBot added the Z-EndToEndBenchCI Tag a PR to run benchmark CI label Jun 28, 2024
zhassan-aws
zhassan-aws reviewed Jun 28, 2024
View reviewed changes

@zhassan-awszhassan-aws left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Thanks. Should the title say "upgrade to 6/28" instead of 6/26?

Comment threadtests/perf/s2n-quic
Comment threadcprover_bindings/src/goto_program/expr.rs Outdated
Comment threadcprover_bindings/src/goto_program/expr.rs
Comment threadcprover_bindings/src/goto_program/expr.rs
Comment threadcprover_bindings/src/irep/to_irep.rs
Comment threadcprover_bindings/src/irep/to_irep.rs
Comment threadcprover_bindings/src/irep/to_irep.rs Outdated
Comment threadcprover_bindings/src/irep/to_irep.rs Outdated
tautschnig
tautschnig reviewed Jun 28, 2024
View reviewed changes
Comment threadcprover_bindings/src/goto_program/mod.rs
Comment threadcprover_bindings/src/goto_program/typ.rs Outdated
Comment threadcprover_bindings/src/irep/to_irep.rs Outdated
Comment threadkani-compiler/src/kani_middle/attributes.rs
@jaisnanjaisnan changed the title Add support for f16 and f128 for toolchain upgrade to 6/26Add support for f16 and f128 for toolchain upgrade to 6/28Jun 28, 2024
@jaisnan
jaisnan requested a review from zhassan-awsJune 28, 2024 18:09
tautschnig
tautschnig reviewed Jun 28, 2024
View reviewed changes
Comment threadcprover_bindings/src/goto_program/typ.rs
zhassan-aws
zhassan-aws approved these changes Jun 28, 2024
View reviewed changes
Comment threadcprover_bindings/src/irep/to_irep.rs Outdated
celinval
celinval reviewed Jun 28, 2024
View reviewed changes

@celinvalcelinval left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Can you please add some tests?

@zhassan-aws

zhassan-aws commented Jun 28, 2024

Copy link
Copy Markdown
Contributor

Can you please add some tests?

I was going to mention this in my overall comment, but completely forgot 🙈

celinval
celinval previously requested changes Jun 28, 2024
View reviewed changes

@celinvalcelinval left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Can you at least extend this test to include the new floating points?

https://github.com/model-checking/kani/blob/main/tests/kani/FloatingPoint/main.rs

This was referenced Jun 28, 2024
Open
Closed
@jaisnan
jaisnan requested a review from celinvalJune 28, 2024 22:06
@tautschnig
tautschnig dismissed celinval’s stale reviewJuly 1, 2024 18:28

Review is stale as tests have been added.

@adpaco
adpaco enabled auto-merge (squash) July 1, 2024 19:09
@adpaco
adpaco merged commit d55f25b into model-checking:mainJul 1, 2024
@jaisnan
jaisnan deleted the toolchain-upgrade-3303 branch July 1, 2024 19:21
@github-actionsgithub-actionsBot mentioned this pull request Sep 9, 2024
Closed
Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@tautschnigtautschnigtautschnig approved these changes
@celinvalcelinvalAwaiting requested review from celinval
+2 more reviewers
@adpacoadpacoadpaco approved these changes
@zhassan-awszhassan-awszhassan-aws approved these changes
Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

Z-EndToEndBenchCITag a PR to run benchmark CI

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Toolchain upgrade to nightly-2024-06-28 failed

5 participants

@jaisnan@zhassan-aws@tautschnig@celinval@adpaco