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

Enable the option enforce determinism for the verify command #5632

Merged

Conversation

keyboardDrummer
Copy link
Member

Description

  • Enable the option enforce determinism for the verify command

How has this been tested?

  • Updated the tests ForbidNonDeterminism.dfy and ForbidNonDeterminismCompile.dfy

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

@keyboardDrummer keyboardDrummer enabled auto-merge (squash) July 18, 2024 14:51
@keyboardDrummer keyboardDrummer force-pushed the verifyEnforceDeterminism branch from 5e13a9b to febc1b7 Compare August 8, 2024 13:26
@keyboardDrummer keyboardDrummer requested review from robin-aws and removed request for RustanLeino and robin-aws August 13, 2024 09:38
Copy link
Member

@MikaelMayer MikaelMayer left a comment

Choose a reason for hiding this comment

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

I like it that enforcing determinism is no longer restricted to a compiler error but is also visible during resolution. A few comments to discuss, otherwise no big deal.

@@ -161,7 +161,7 @@ jobs:
output: both
# Fail if less than 86% total coverage, measured across all packages combined.
# Report "yellow" status if less than 90% total coverage.
thresholds: '86 90'
thresholds: '85 90'
Copy link
Member

Choose a reason for hiding this comment

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

I would like to see this threshold lowering accepted by @atomb. If I remember correctly, we wanted to not lower this threshold but gradually increase it when we test more and more code.

Copy link
Member Author

@keyboardDrummer keyboardDrummer Aug 13, 2024

Choose a reason for hiding this comment

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

I think ideally you would not measure a percentage but the absolute number of uncovered lines, and have a threshold on that, so that any added code must be covered, and in case some is uncovered you must explicitly update the threshold to confirm that.

If we would measure like that, this PR wouldn't have to update anything since AFAIK it does not add uncovered lines, just removes already covered ones, which lower the percentage.

Copy link
Member

Choose a reason for hiding this comment

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

I don't get it. If you measure an absolute number of uncovered lines, you'll have to update this absolute number for every PR, right? Otherwise, if you only add uncovered lines of code, it would not complain which is not desirable.

Copy link
Member Author

Choose a reason for hiding this comment

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

I don't get it. If you measure an absolute number of uncovered lines, you'll have to update this absolute number for every PR, right?

If you only add covered lines, then the uncovered line count does not change, so you would not have to update anything.

Copy link
Member

Choose a reason for hiding this comment

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

If you only add covered lines, then the coverage percentage is automatically going up, so you wouldn't have to update anything if the threshold stays the same. The covered line percentage is an average, adding anything above this average will increase the average, which thus will remain above the threshold. Am I missing something?

@@ -537,7 +537,9 @@ public enum DefaultFunctionOpacityOptions {

DafnyOptions.RegisterLegacyBinding(EnforceDeterminism, (options, value) => {
options.ForbidNondeterminism = value;
options.DefiniteAssignmentLevel = 4;
if (!options.Get(RelaxDefiniteAssignment)) {
options.DefiniteAssignmentLevel = 4;
Copy link
Member

Choose a reason for hiding this comment

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

Please document this relationship in the attributes documentation if not already done

Copy link
Member Author

Choose a reason for hiding this comment

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

Can you elaborate? How does this code relate to attributes? I don't see a DefiniteAssignmentLevel attribute

Copy link
Member

Choose a reason for hiding this comment

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

Oh I see. Thanks for clarifying. So essentially, you're fixing an error of mapping the new CLI to the old CLI, correct?

Copy link
Member Author

Choose a reason for hiding this comment

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

Yes

MikaelMayer
MikaelMayer previously approved these changes Aug 14, 2024
MikaelMayer
MikaelMayer previously approved these changes Aug 14, 2024
@@ -161,7 +161,7 @@ jobs:
output: both
# Fail if less than 86% total coverage, measured across all packages combined.
# Report "yellow" status if less than 90% total coverage.
thresholds: '86 90'
thresholds: '85 90'
Copy link
Member

Choose a reason for hiding this comment

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

If you only add covered lines, then the coverage percentage is automatically going up, so you wouldn't have to update anything if the threshold stays the same. The covered line percentage is an average, adding anything above this average will increase the average, which thus will remain above the threshold. Am I missing something?

@keyboardDrummer keyboardDrummer merged commit 8de6d00 into dafny-lang:master Aug 15, 2024
21 checks passed
@keyboardDrummer
Copy link
Member Author

keyboardDrummer commented Aug 15, 2024

If you only add covered lines, then the coverage percentage is automatically going up, so you wouldn't have to update anything if the threshold stays the same. The covered line percentage is an average, adding anything above this average will increase the average, which thus will remain above the threshold. Am I missing something?

This does not work when someone removes covered lines, which should be fine.

Another disadvantage of using percentages, which I think might be the bigger one, is that when adding new code, the new code only needs to be covered to the same percentage as the existing code.

@keyboardDrummer keyboardDrummer deleted the verifyEnforceDeterminism branch August 15, 2024 12:58
atomb added a commit that referenced this pull request Aug 19, 2024
### Description

After #5632, Dafny started complaining about traits lacking constructors
(which they can't have) when `--enforce-determinism` was enabled. This
changes back to the previous behavior of warning only about classes
without constructors.

### How has this been tested?

Updated `dafny0/ForbidNondeterminismResolve.dfy` to include a trait
declaration.

By submitting this pull request, I confirm that my contribution
is made under the terms of the MIT license.
dnezam pushed a commit to dnezam/dafny that referenced this pull request Sep 21, 2024
### Description

After dafny-lang#5632, Dafny started complaining about traits lacking constructors
(which they can't have) when `--enforce-determinism` was enabled. This
changes back to the previous behavior of warning only about classes
without constructors.

### How has this been tested?

Updated `dafny0/ForbidNondeterminismResolve.dfy` to include a trait
declaration.

By submitting this pull request, I confirm that my contribution
is made under the terms of the MIT license.
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