Add BoundedInts to DafnyStdLibs #4713

keyboardDrummer · 2023-10-25T13:29:18Z

Description

Add BoundedInts.dfy, BoundedInts.md and BoundedIntExamples.dfy from https://github.com/dafny-lang/libraries to https://github.com/dafny-lang/dafny/tree/master/Source/DafnyStandardLibraries
For Go, allows customizing the dummy value that is used for an {:extern} module, using a new undocumented, only internally used, {:member <name>, <isType>} attribute. This is necessary to let the BoundedIntExamples.dfy pass, because FunctionExamples.dfy, which is part of the same project, does not use the {:extern} module, so Go gives an unused import error. In the future I expect that we change our Go compiler so it only emits imports that are used, which makes the {:member} attribute obsolete and allows us to remove support for it from our codebase without breaking anyone.

How has this been tested?

The examples file serves as a test. It contains an extern method that demonstrates which native types the Dafny compiler picks when using int32 in Dafny.

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

…oundedInts

robin-aws

Looks great and I like the testing approach! Just a couple of thoughts for later and a question.

robin-aws · 2023-10-27T16:14:27Z

Source/DafnyStandardLibraries/examples/WrappersExamples.dfy

@@ -1,172 +1,168 @@
-module Demo {
+import opened DafnyStdLibs.Wrappers


Good change, but wow did GitHub ever mess up the diff something terrible. :)

robin-aws · 2023-10-27T16:16:18Z

Source/DafnyStandardLibraries/examples/BoundedIntExamples.dfy

+
+module {:extern} Externs {
+ import opened DafnyStdLibs.BoundedInts
+ class {:extern} NonDefault {


Why "NonDefault"?

My impression is that for Java an extern should not be in the default class since there are no partial classes.

Oh Java does support mixed Dafny and target classes: https://github.com/dafny-lang/dafny/blob/master/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Mixed.java And that works fine with default classes, it just looks weird because of the __default name.

This way is just fine though, I just didn't get why the class was named what it was.

robin-aws · 2023-10-27T16:18:07Z

Source/DafnyStandardLibraries/Makefile

+ $(DAFNY) test -t:cs build/stdlibexamples.doo examples/BoundedInts/NonDefault.cs --output:build/stdlibexamples
+ $(DAFNY) test -t:java build/stdlibexamples.doo examples/BoundedInts/Externs/NonDefault.java --output:build/stdlibexamples
+ $(DAFNY) test -t:go build/stdlibexamples.doo examples/BoundedInts/NonDefault.go --output:build/stdlibexamples
+ $(DAFNY) test -t:py build/stdlibexamples.doo examples/BoundedInts/NonDefault.py --output:build/stdlibexamples
+ $(DAFNY) test -t:js build/stdlibexamples.doo examples/BoundedInts/NonDefault.js --output:build/stdlibexamples


Fine for this change but probably worth replacing with a find of all files of the right extension in the next one, and before too long with project file support for this. :)

Or look into target specific options in the project file

robin-aws · 2023-10-27T16:24:00Z

Almost forgot, make sure you update https://github.com/dafny-lang/dafny/tree/master/Source/DafnyStandardLibraries#available-libraries too!

Might be worth adding a tiny Functions.md for that too.

robin-aws

Just a few more nits, nothing hard-blocking. Happy with the {:dummyImportMember} name. Do update the PR description so the commit message is accurate. :)

robin-aws · 2023-10-31T17:28:18Z

Source/DafnyStandardLibraries/examples/BoundedIntExamples.dfy

+
+module {:extern} Externs {
+ import opened DafnyStdLibs.BoundedInts
+ class {:extern} NonDefault {


Oh Java does support mixed Dafny and target classes: https://github.com/dafny-lang/dafny/blob/master/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Mixed.java And that works fine with default classes, it just looks weird because of the __default name.

This way is just fine though, I just didn't get why the class was named what it was.

robin-aws · 2023-11-03T15:27:32Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/wishlist/GoModule.dfy

@@ -2,7 +2,7 @@
 // RUN: %exits-with 3 %dafny /compile:3 /unicodeChar:0 /spillTargetCode:2 "%s" /compileTarget:go 2> "%t"
 // note: putting /compileTarget:go after "%s" overrides user-provided option
 // RUN: %OutputCheck --file-to-check "%t" "%s"
-// CHECK: GoModuleConversions.go:10:3: "net/url" imported and not used
+// CHECK: undefined: GoModuleConversions.ParseURL


Not clear on why this is the error we're getting now, but not a blocker since this is just a negative test.

robin-aws · 2023-11-03T15:42:37Z

Source/DafnyCore/Compilers/GoLang/Compiler-go.cs

+ } else {
+ isType = true;
+ if (import.ExternModule != null) {
+ var attributes = Attributes.Find(import.ExternModule.Attributes, "dummyImportMember");


Definitely glad we're not documenting this officially, but it might be worth adding a note on this attribute to https://github.com/dafny-lang/dafny/blob/master/Source/DafnyStandardLibraries/CONTRIBUTING.md, just so anyone that might need to use it is at least aware of how it works.

robin-aws · 2023-11-03T15:46:28Z

Source/DafnyCore/Compilers/SinglePassCompiler.cs

@@ -167,12 +167,14 @@ public abstract class SinglePassCompiler {
 /// call to the instance Main method in the enclosing class.
 /// </summary>
 protected abstract ConcreteSyntaxTree CreateStaticMain(IClassWriter wr, string argsParameterName);
- protected abstract ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, bool isExtern, string/*?*/ libraryName, ConcreteSyntaxTree wr);
+ protected abstract ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,


Definitely feels a little weird to have a parameter that is "the module being created, but only passed if it's an extern". Consider keeping isExtern and theModule as separate parameters.

robin-aws · 2023-11-03T15:48:03Z

Source/DafnyCore/AST/Members/ICodeContext.cs

Just for my own understanding, are the AST changes unrelated cleanup or necessary somehow?

Unrelated, yes

keyboardDrummer added 5 commits October 25, 2023 15:19

Add BoundedInts to DafnyStdLibs

fddf31f

Use bounded ints in externs in BoundedIntExamples

e67f203

Merge branch 'master' into boundedInts

501df4f

Fix .md file

9cd59e4

Merge branch 'boundedInts' of github.com:keyboardDrummer/dafny into b…

d1a66e1

…oundedInts

keyboardDrummer enabled auto-merge (squash) October 26, 2023 12:36

robin-aws reviewed Oct 27, 2023

View reviewed changes

robin-aws mentioned this pull request Oct 27, 2023

Relations #4709

Merged

keyboardDrummer added 4 commits October 30, 2023 10:49

update /DafnyStandardLibraries/README.md

e5313e7

Merge branch 'master' into boundedInts

0c9b812

Merge remote-tracking branch 'origin/master' into boundedInts

a56eb7e

Fix for Go compiler

3067c61

keyboardDrummer requested a review from robin-aws October 31, 2023 10:34

keyboardDrummer added 4 commits October 31, 2023 11:50

More Go Compiler fixes

4bad250

Fix for Go

4aa7f0b

Go fixes

c33b8ef

Go fixes

6f032e3

keyboardDrummer force-pushed the boundedInts branch from 567ada9 to 6f032e3 Compare October 31, 2023 15:58

robin-aws mentioned this pull request Oct 31, 2023

Go compiler inserts imports of unused modules #2953

Open

keyboardDrummer added 4 commits November 1, 2023 12:29

Do not use the default dummy for external modules

5038892

Merge remote-tracking branch 'origin/master' into boundedInts

6522a7e

Update gradle

a6a4fa5

Rename member attribute

ef5cd0d

robin-aws approved these changes Nov 3, 2023

View reviewed changes

keyboardDrummer merged commit d4109e0 into dafny-lang:master Nov 3, 2023
20 checks passed

keyboardDrummer deleted the boundedInts branch November 6, 2023 09:24

keyboardDrummer mentioned this pull request Nov 6, 2023

Follow-up changes related to BoundedInts #4740

Open

robin-aws mentioned this pull request Nov 8, 2023

Standard library: BoundedInts #4643

Closed

robin-aws mentioned this pull request Nov 16, 2023

feat: Per-backend code support in standard libraries, FileIO library #4790

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add BoundedInts to DafnyStdLibs #4713

Add BoundedInts to DafnyStdLibs #4713

keyboardDrummer commented Oct 25, 2023 •

edited

Loading

robin-aws left a comment

robin-aws Oct 27, 2023

robin-aws Oct 27, 2023

keyboardDrummer Oct 30, 2023

robin-aws Oct 31, 2023

robin-aws Oct 27, 2023

keyboardDrummer Oct 30, 2023

robin-aws commented Oct 27, 2023

robin-aws left a comment

robin-aws Oct 31, 2023

robin-aws Nov 3, 2023

robin-aws Nov 3, 2023

robin-aws Nov 3, 2023

robin-aws Nov 3, 2023

keyboardDrummer Nov 6, 2023

		@@ -1,172 +1,168 @@
		module Demo {
		import opened DafnyStdLibs.Wrappers

Add BoundedInts to DafnyStdLibs #4713

Add BoundedInts to DafnyStdLibs #4713

Conversation

keyboardDrummer commented Oct 25, 2023 • edited Loading

Description

How has this been tested?

robin-aws left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

robin-aws commented Oct 27, 2023

robin-aws left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer commented Oct 25, 2023 •

edited

Loading