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.

Sign up for GitHub

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

Jump to bottom

Java backend not handling well module and datatype homonyms #6014

Closed
olivier-aws opened this issue Jan 3, 2025 · 0 comments · Fixed by #6016 · May be fixed by olivier-aws/dafny#1
Closed

Java backend not handling well module and datatype homonyms #6014

olivier-aws opened this issue Jan 3, 2025 · 0 comments · Fixed by #6016 · May be fixed by olivier-aws/dafny#1
Assignees
@olivier-aws
Labels
invalid translated code The compiler generates invalid code, making the the target language infrastructure crash kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: java Dafny's Java transpiler and its runtime

Comments

@olivier-aws
Copy link
Contributor

Dafny version

4.9.1

Code to produce this issue

module State {

  datatype State = Whatever

}

module Foo {

   import opened State

   const bar: State

   method Main() {
     print "Hello!\n";
  }
}

Command to run and resulting output

dafny build -t:java file.dfy

What happened?

Dafny program verifier finished with 0 verified, 0 errors
Picked up JAVA_TOOL_OPTIONS: -Dlog4j2.formatMsgNoLookups=true
file-java/Foo/__default.java:18: error: cannot find symbol
  public static State.State bar()
                     ^
  symbol:   class State
  location: class State
file-java/State/State.java:37: error: cannot find symbol
  private static final State theDefault = State.State.create();
                                               ^
  symbol:   variable State
  
  ...

This is similar to the error reported for CS backend in #5746

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

Mac
@olivier-aws olivier-aws added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: java Dafny's Java transpiler and its runtime invalid translated code The compiler generates invalid code, making the the target language infrastructure crash labels Jan 3, 2025
@olivier-aws olivier-aws self-assigned this Jan 3, 2025
@olivier-aws olivier-aws linked a pull request Jan 3, 2025 that will close this issue
[DRAFT] Do not generate import of modules in Java olivier-aws/dafny#1
Draft
This was referenced Jan 3, 2025
Draft
Merged
@olivier-aws olivier-aws mentioned this issue Jan 6, 2025
Merged
olivier-aws added a commit that referenced this issue Jan 11, 2025
@olivier-aws @MikaelMayer
Fix name clash in generated CS files when module and types have same …
0a33545 
…name (#6019)

### What was changed?
This change updates the CS code generated from Dafny to fix name clashes
between namespace and class when a module defines a datatype with the
same name. On the example for
#6014, we have:

```
module A {

  datatype A = Foo. // Notice the name of the datatype is the name of the module

}

module B {

   import opened A

   const bar: A

   method Main() {
     print "Hello!\n";
  }
}

```

which generated the code (simlified for readability)

```
namespace A {

  public interface _IA {
    bool is_Foo { get; }
    _IA DowncastClone();
  }
  public class A : _IA {
    public A() {
    }
    // [...]

    public static _IA create() {
      return new A();
    }

    private static readonly A._IA theDefault = create();

   // [...]

    }
  }
} // end of namespace A

namespace B {

  public partial class __default {
    public static void _Main(Dafny.ISequence<Dafny.ISequence<Dafny.Rune>> __noArgsParameter)
    {
      Dafny.Helpers.Print((Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Hello!\n")).ToVerbatimString(false));
    }
    public static A._IA bar { get {
      return A.A.Default();
    } }
  }
} // end of namespace B

```


The expression `A._IA theDefault` does not compile in C#, as the first
A. is resolved to be the name of the class and not the name of the
namespace. One solution could be to ensure we have `_IA` here instead of
`A._IA` as for the `create` method, but the code to generate this type
name is used at other places where the `A._IA` is required (e.g in `
bar` method in `namespace B`).

This change changes the name of the namespace `A` to `_NA` when there is
a name clash with a datatype declared in `A`.

### How has this been tested?
Updated test gith-issues-6014.dfy


<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: Mikaël Mayer <[email protected]>
@olivier-aws olivier-aws mentioned this issue Jan 15, 2025
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@olivier-aws olivier-aws

Labels
invalid translated code The compiler generates invalid code, making the the target language infrastructure crash kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: java Dafny's Java transpiler and its runtime
Projects
None yet
Milestone
No milestone
1 participant
@olivier-aws