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

[Python] Nested set comprehension results in invalid generated code #5285

Closed
lucasmcdonald3 opened this issue Apr 1, 2024 · 0 comments · Fixed by #5287
Closed

[Python] Nested set comprehension results in invalid generated code #5285

lucasmcdonald3 opened this issue Apr 1, 2024 · 0 comments · Fixed by #5287
Assignees
@fabiomadge
Labels
during 4: bad execution of correct program A bug in the Dafny compiler that causes a correct Dafny program to execute incorrectly kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: python Dafny's Python transpiler and its runtime

Comments

@lucasmcdonald3
Copy link
Contributor

lucasmcdonald3 commented Apr 1, 2024 •
edited
Loading

Dafny version

4.6.0

Code to produce this issue

module AnyModule {

    datatype someDatatype = 
        | SomeConcreteDatatype(
            someString: string
        )

    function someMethod(someString: string) : string{
        someString
    }

    const someConst := 
        set
            someString <- {"a"},
            someSet
            <- set
                s <- someMethod(someString)
                :: s
    :: 
    SomeConcreteDatatype(someString := someString)

}

Command to run and resulting output

lucmcdon@88665a0bd366 any_module % dafny translate py AnyModule.dfy

Dafny program verifier finished with 0 verified, 0 errors
lucmcdon@88665a0bd366 any_module % cd AnyModule-py 
lucmcdon@88665a0bd366 AnyModule-py % python3
Python 3.11.6 (v3.11.6:8b6ee5ba3b, Oct  2 2023, 11:18:21) [Clang 13.0.0 (clang-1300.0.29.30)] on darwin
Type "help", "copyright", "credits" or "license" for more information.
>>> import AnyModule
>>> AnyModule.default__.someConst
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "/Library/Frameworks/Python.framework/Versions/3.11/lib/python3.11/site-packages/_dafny/__init__.py", line 14, in __get__
    return classmethod(self.fget).__get__(None, owner)()
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/Users/lucmcdon/Desktop/dafny_test/any_module/AnyModule-py/AnyModule.py", line 51, in someConst
    return iife0_()
           ^^^^^^^^
  File "/Users/lucmcdon/Desktop/dafny_test/any_module/AnyModule-py/AnyModule.py", line 39, in iife0_
    if ((d_0_someString_) in (_dafny.Set({_dafny.SeqWithoutIsStrInference(map(_dafny.CodePoint, "a"))}))) and ((d_2_someSet_) in (iife2_()
                                                                                                                                  ^^^^^^^^
  File "/Users/lucmcdon/Desktop/dafny_test/any_module/AnyModule-py/AnyModule.py", line 46, in iife2_
    for compr_3_ in (default__.someMethod(d_0_someString_)).Elements:
                                          ^^^^^^^^^^^^^^^
NameError: name 'd_0_someString_' is not defined

What happened?

I expected to see some valid output (ex a Set(["a"])); instead I ran into a NameError.
The d_0_someString_ variable is not defined in the scope of a child method, so it cannot be accessed.
The Python code generation generation may need to define this variable at a higher scope, or may need to pass this variable to the child method iife2.

(This is a lightweight example reproducing a similar error I encountered in some AWS Cryptography MPL code: link)
(My grasp of set comprehension syntax is poor, so there is probably a more minimal example.)

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

Mac
@lucasmcdonald3 lucasmcdonald3 added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label Apr 1, 2024
@fabiomadge fabiomadge self-assigned this Apr 2, 2024
@fabiomadge fabiomadge mentioned this issue Apr 2, 2024
Merged
@fabiomadge fabiomadge added lang: python Dafny's Python transpiler and its runtime during 4: bad execution of correct program A bug in the Dafny compiler that causes a correct Dafny program to execute incorrectly labels Apr 2, 2024
robin-aws pushed a commit that referenced this issue Apr 2, 2024
@fabiomadge
fix: Invalid Python code for nested set and map comprehensions (#5287)
c931468 
Fixes #5285.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@fabiomadge fabiomadge

Labels
during 4: bad execution of correct program A bug in the Dafny compiler that causes a correct Dafny program to execute incorrectly kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: python Dafny's Python transpiler and its runtime
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

fix: Invalid Python code for nested set and map comprehensions fabiomadge/dafny
2 participants
@fabiomadge @lucasmcdonald3