fix: Forbid recursive function uses in decreases clauses #6045

RustanLeino · 2025-01-11T02:35:14Z

Fixes #6043

This PR changes two verification checks into resolution checks:

use of a function in a decreases clause in the function's SCC
use of naked functions inside an SCC

The first of these was omitted in the recent CanCall PR. Hence, this PR fixes that regression.

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

Note, the “function specification” SelectWF check was never reached (and was not in the test suite).

Fixes dafny-lang#6043

typerSniper · 2025-01-13T19:33:26Z

Source/DafnyCore/Resolver/FunctionEntanglementChecks_Visitor.cs

+      }
+    }
+  }
+}


need new line here.

typerSniper · 2025-01-13T19:46:28Z

Source/DafnyCore/Resolver/FunctionEntanglementChecks_Visitor.cs

+
+namespace Microsoft.Dafny;
+
+class FunctionEntanglementChecks_Visitor : ResolverBottomUpVisitor {


Minor Nitpick: Not sure Entanglement is the right word here. Following the implementation, two functions are entangled when they are in the same SCC and one uses the other either in a naked fashion or in a decreases clause. But the fact that they are in the SCC means that they depend on one another and already feel entangled. Maybe DetectUnsoundFunctionReferences or DUFR (pronounced as duffer 😂)

# Conflicts: # Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/parser_combinators.dfy.expect # Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-847.dfy.expect # Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Naked.dfy.expect

typerSniper · 2025-01-13T23:17:02Z

Looks good!

keyboardDrummer · 2025-01-14T10:13:18Z

Source/DafnyCore/Resolver/DetectUnsoundFunctionReferences_Visitor.cs

+
+namespace Microsoft.Dafny;
+
+class DetectUnsoundFunctionReferences_Visitor : ResolverBottomUpVisitor {


Why the _ in the name? I think that's outside of C# conventions. Does Rider not suggest to remove it?

I had followed the convention used by other _Visitor classes in the Dafny sources. But I agree that's outside C# conventions. So, I now renamed all classes in Dafny to remove _'s.

keyboardDrummer · 2025-01-14T10:15:41Z

Source/DafnyCore/Resolver/DetectUnsoundFunctionReferences_Visitor.cs

+
+class DetectUnsoundFunctionReferences_Visitor : ResolverBottomUpVisitor {
+  private readonly ICallable context;
+  public bool DoDecreasesChecks;


I know it doesn't matter much, but I think C# developers generally prefer auto properties over public fields, at least I do. One example: you can put a breakpoint on a property getter/setter, but not on a field read/write.

I made it private, as per the suggestion below.

keyboardDrummer · 2025-01-14T10:16:53Z

Source/DafnyCore/Resolver/DetectUnsoundFunctionReferences_Visitor.cs

+      }
+    }
+
+    if (DoDecreasesChecks && expr is FunctionCallExpr callExpr) {


Please merge the conditions to reduce nesting, and consider inverting the condition to get an early return and fully remove the nesting.

I unnested the if's.

keyboardDrummer · 2025-01-14T10:17:57Z

Source/DafnyCore/Resolver/ModuleResolver.cs

        FillInPostConditionsAndBodiesOfPrefixLemmas(declarations);
      }

+      // A function is not allowed to be used naked in its own SCC. Also, a function is not allowed to be used


What does the term naked here mean?

It means the function name is used without applying it to arguments. (This nomenclature is not new in this PR.) I clarified in the comment.

keyboardDrummer · 2025-01-14T10:19:08Z

Source/DafnyCore/Resolver/ModuleResolver.cs

+      // in any way inside a "decreases" clause its its own SCC.
+      foreach (var function in ModuleDefinition.AllFunctions(declarations)) {
+        var visitor = new DetectUnsoundFunctionReferences_Visitor(this, function);
+        visitor.Visit(function);


If this visit/doDecreasesChecks/visit pattern is the only correct way to use DetectUnsoundFunctionReferences_Visitor, then it would be better to move this into a static method in that class, and make the constructor and DoDecreasesChecks field private.

keyboardDrummer · 2025-01-14T10:20:13Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TailCalls.dfy.expect

 TailCalls.dfy(126,19): Error: the recursive call to 'Compute' is not tail recursive because the actual type argument is not the formal type parameter 'G'
 TailCalls.dfy(139,17): Error: the recursive call to 'Run' is not tail recursive because the actual type argument 1 is not the formal type parameter 'G'
-30 resolution/type errors detected in TailCalls.dfy
+TailCalls.dfy(171,13): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.


Can we avoid the use of the word naked here? Can I find more information on what the problem is and the possible solution? Maybe add a reference to documentation?

I left this as is. This PR does not introduce the phrase "naked function". It would be good to revisit, and indeed to say something about it in the documentation.

Because `CanCall` is now used everywhere, the Boogie variable `$FunctionContextHeight` is no longer needed. This PR also removes the variable `$ModuleContextHeight`, which has been unused for some time now. Depends on #6045 <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

RustanLeino added 4 commits January 10, 2025 18:31

Change naked check from verifier to resolver

b90d350

Note, the “function specification” SelectWF check was never reached (and was not in the test suite).

Update tests to reflect resolution (not verifier) checks

0547e0b

fix: Forbid recursive function uses in decreases clauses

eff7b7a

Fixes dafny-lang#6043

chore: Improve C#

487f061

RustanLeino requested a review from typerSniper January 11, 2025 02:35

RustanLeino added 2 commits January 10, 2025 21:28

Fix up tests

6d39cfb

Adjust test output (good?)

980dc0d

RustanLeino mentioned this pull request Jan 11, 2025

Remove function-context-height variable in Boogie encoding #6046

Merged

typerSniper reviewed Jan 13, 2025

View reviewed changes

RustanLeino added 5 commits January 13, 2025 14:38

Add tests (forgot to git-add these before)

800654f

Add newline at EOF

85346c8

Rename class

579ca74

Merge branch 'master' into issue-6043

aadce6b

typerSniper previously approved these changes Jan 13, 2025

View reviewed changes

keyboardDrummer reviewed Jan 14, 2025

View reviewed changes

RustanLeino added 6 commits January 14, 2025 13:43

Rename classes and files to remove underscores

6f33de4

Unnested if’s

8f4284f

Clarify comment

c4de62e

Add public static DetectUnsoundFunctionReferencesVisitor.Check method

ff42711

Merge branch 'master' into issue-6043

bbb8f80

Adjust to new source locations in error messages

ed736f5

RustanLeino dismissed typerSniper’s stale review via ed736f5 January 14, 2025 22:10

RustanLeino enabled auto-merge (squash) January 14, 2025 23:18

keyboardDrummer approved these changes Jan 15, 2025

View reviewed changes

RustanLeino merged commit 6afa6d5 into dafny-lang:master Jan 15, 2025
22 checks passed

RustanLeino deleted the issue-6043 branch January 15, 2025 17:58

+                    }
+                  }
+                }
+              }

                
                    No newline at end of file


		namespace Microsoft.Dafny;

		class FunctionEntanglementChecks_Visitor : ResolverBottomUpVisitor {


		namespace Microsoft.Dafny;

		class DetectUnsoundFunctionReferences_Visitor : ResolverBottomUpVisitor {

fix: Forbid recursive function uses in decreases clauses #6045

fix: Forbid recursive function uses in decreases clauses #6045

Uh oh!

Conversation

RustanLeino commented Jan 11, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

typerSniper commented Jan 13, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants