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

Topological order not computed correctly when multiple dfy files present in the command-line #5728

Open
MikaelMayer opened this issue Aug 28, 2024 · 0 comments
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

Comments

@MikaelMayer
Copy link
Member

Dafny version

latest-nightly

Code to produce this issue

// File1.dfy

replaceable module X {
  method getMessage() returns (s: string)
}

module XGo replaces module X {
  method getMessage() returns (s: string) {
    s := "I'm in XGo";
  }
}

// File2.dfy
module Y {
  import X;
  method Test() {
    var message := X.getMessage();
    print message;
  }
}

method Main() {
  Y.Test();
}

Command to run and resulting output

> dafny build -t:lib File2.dfy File1.dfy --output File21.doo

Makes a .doo file containing a program in which module XGo appears after module Y. If you run it in Go:

> dafny run -t:go File21.doo

produces an error in the go files saying module XGo not found because doo files are assumed to be in topological order.

> dafny build -t:lib File1.dfy File2.dfy --output File12.doo
> dafny run -t:go File21.doo

works as expected.

What happened?

The module order when emitting doo files is not topologically sorted when multiple files are provided, it's the order of the provided files.
Historically, this is why some systems are not able to build the .doo files locally, because the find order of the external modules is different. @atomb reported a find order of:

./Concurrent-go.dfy
./Concurrent-notarget-java-cs-js-go-py.dfy
./FileIOInternalExterns-notarget-java-cs-js-go-py.dfy
./FileIOInternalExterns-go.dfy
./FileIO-notarget-java-cs-js-go-py.dfy
`` 

whereas my find order returned:

./Concurrent-go.dfy
./Concurrent-notarget-java-cs-js-go-py.dfy
./FileIO-notarget-java-cs-js-go-py.dfy
./FileIOInternalExterns-go.dfy
./FileIOInternalExterns-notarget-java-cs-js-go-py.dfy


which caused the generated doo files to not work with the CI, but moreover go projects cannot compile with my generated doo files (I'm on Windows using git bash).

### What type of operating system are you experiencing the problem on?

Windows
@MikaelMayer MikaelMayer added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label Aug 28, 2024
MikaelMayer added a commit that referenced this issue Sep 3, 2024
### Description
Merging the release 4.8.0 branch into master It brings several
modifications that were deemed necessary
- Updated the doo files from the DafnyStandardLibraries,
- Updated doo files and dtr files from the test suite
- Renamed dfy files for externs so that they are in the same order and
don't cause issue as a workaround for
#5728 and updated README about
the naming of those files
- Added %rm %mv and %cp command which are used in tests but not
available on every windows machine (mine included)
- Added support for any exit code so that `%rm` won't fail if a file or
a folder does not exist (which is the case the first time)
- Added ability to run a command within a given folder as some commands
would not run on my Windows.
- Added `-f` option to cp and mv to be able to run the same test
multiple times
- Added missing sources to recompile multiple doo files in the test
suite.

### How has this been tested?
Tests are passing on the CI and previously offending tests are also
passing on my Windows machine.

<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>

---------

Co-authored-by: Aaron Tomb <[email protected]>
Co-authored-by: Siva Somayyajula <[email protected]>
Co-authored-by: Siva Somayyajula <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
Projects
None yet
Development

No branches or pull requests

1 participant