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

Dafny's verifier incorrectly uses :extern names #1984

Closed
cpitclaudel opened this issue Apr 7, 2022 · 0 comments · Fixed by #1986
Closed

Dafny's verifier incorrectly uses :extern names #1984

cpitclaudel opened this issue Apr 7, 2022 · 0 comments · Fixed by #1986
Assignees
@cpitclaudel
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator)

Comments

@cpitclaudel
Copy link
Member

For example, this is rejected:

method {:extern "test"} testInt(i: int)
method {:extern "test"} testBool(b: bool)
$ Dafny "git-issue-1984.dfy"
git-issue-1984.dfy(5,24): Error: more than one declaration of procedure name: CheckWellformed$$_module.__default.test
git-issue-1984.dfy(5,24): Error: more than one declaration of procedure name: Call$$_module.__default.test
@cpitclaudel cpitclaudel added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator) labels Apr 7, 2022
cpitclaudel added a commit that referenced this issue Apr 8, 2022
@cpitclaudel
fix: Don't use CompileName outside of the compilers
0f36e31 
* Source/Dafny/AST/DafnyAst.cs:

  (Declaration.SanitizedName, TypeParameter.SanitizedName,
   TupleTypeDecl.SanitizedName, NonglobalVariable.SanitizedName,
   LocalVariable.SanitizedName, Formal.SanitizedName):
  New property

  (ModuleDefinition.SanitizedName):
  New property (created by splitting off the non-extern parts of CompileName)

  (Declaration.CompileName, ModuleDefinition.CompileName):
  Use SanitizedName

  (TypeParameter.CompileName, TupleTypeDecl.CompileName,
   NonglobalVariable.CompileName, LocalVariable.CompileName):
  Alias to SanitizedName

  (ModuleExportDecl, ModuleDefinition.VisibilityScope):
  Use SanitizedName when creating the VisibilityScope

  (ModuleDefinition.FullSanitizedName, DataTypeDecl.FullSanitizedName):
  Use SanitizedName, not CompileName

  (NonglobalVariable.CompilerizeName):
  Rename to SanitizeName

  (NonglobalVariable.AssignUniqueName, LocalVariable.AssignUniqueName):
  Only assign uniqueName (compileName initialization was duplicated with the
  CompileName getter)

  (FunctionCallFinder.PrintFunctionCallGraph):
  Use SanitizedName, not CompileName

  (ModuleDefinition.RefinementCompileName,
   ModuleDefinition.FullSanitizedRefinementName, MemberDecl.FullNameInContext,
   MemberDecl.FullSanitizedRefinementName, SpecialField.FullCompileName,
   SpecialField.FullNameInContext, SpecialField.FullSanitizedRefinementName):
  Remove unused properties

* Source/Dafny/Verifier/Translator.cs (Translator.Translate):
* Source/DafnyServer/SymbolTable.cs (*):

  Use SanitizedName, not CompileName

* Source/Dafny/Resolver.cs (ResolveProgram):
  Use FullSanitizedName instead of FullCompileName when creating a signature for
  an abstract module (originally changed from .Name to .FullCompileName in
  66b9c19)

Fixes #1984.
@cpitclaudel cpitclaudel mentioned this issue Apr 8, 2022
Merged
@cpitclaudel cpitclaudel self-assigned this Apr 8, 2022
cpitclaudel added a commit that referenced this issue Apr 8, 2022
@cpitclaudel
fix: Don't use CompileName outside of the compilers
3b8c9ef 
* Source/Dafny/AST/DafnyAst.cs:

  (Declaration.SanitizedName, TypeParameter.SanitizedName,
   TupleTypeDecl.SanitizedName, NonglobalVariable.SanitizedName,
   LocalVariable.SanitizedName, Formal.SanitizedName):
  New property

  (ModuleDefinition.SanitizedName):
  New property (created by splitting off the non-extern parts of CompileName)

  (Declaration.CompileName, ModuleDefinition.CompileName):
  Use SanitizedName

  (TypeParameter.CompileName, TupleTypeDecl.CompileName,
   NonglobalVariable.CompileName, LocalVariable.CompileName):
  Alias to SanitizedName

  (ModuleExportDecl, ModuleDefinition.VisibilityScope):
  Use SanitizedName when creating the VisibilityScope

  (ModuleDefinition.FullSanitizedName, DataTypeDecl.FullSanitizedName):
  Use SanitizedName, not CompileName

  (NonglobalVariable.CompilerizeName):
  Rename to SanitizeName

  (NonglobalVariable.AssignUniqueName, LocalVariable.AssignUniqueName):
  Only assign uniqueName (compileName initialization was duplicated with the
  CompileName getter)

  (FunctionCallFinder.PrintFunctionCallGraph):
  Use SanitizedName, not CompileName

  (ModuleDefinition.RefinementCompileName,
   ModuleDefinition.FullSanitizedRefinementName, MemberDecl.FullNameInContext,
   MemberDecl.FullSanitizedRefinementName, SpecialField.FullCompileName,
   SpecialField.FullNameInContext, SpecialField.FullSanitizedRefinementName):
  Remove unused properties

* Source/Dafny/Verifier/Translator.cs (Translator.Translate):
* Source/DafnyServer/SymbolTable.cs (*):

  Use SanitizedName, not CompileName

* Source/Dafny/Resolver.cs (ResolveProgram):
  Use FullSanitizedName instead of FullCompileName when creating a signature for
  an abstract module (originally changed from .Name to .FullCompileName in
  66b9c19)

Fixes #1984.
cpitclaudel added a commit that referenced this issue Apr 8, 2022
@cpitclaudel
fix: Don't use CompileName outside of the compilers (#1986)
785ff02 
* fix: Don't use CompileName outside of the compilers

* Source/Dafny/AST/DafnyAst.cs:

  (Declaration.SanitizedName, TypeParameter.SanitizedName,
   TupleTypeDecl.SanitizedName, NonglobalVariable.SanitizedName,
   LocalVariable.SanitizedName, Formal.SanitizedName):
  New property

  (ModuleDefinition.SanitizedName):
  New property (created by splitting off the non-extern parts of CompileName)

  (Declaration.CompileName, ModuleDefinition.CompileName):
  Use SanitizedName

  (TypeParameter.CompileName, TupleTypeDecl.CompileName,
   NonglobalVariable.CompileName, LocalVariable.CompileName):
  Alias to SanitizedName

  (ModuleExportDecl, ModuleDefinition.VisibilityScope):
  Use SanitizedName when creating the VisibilityScope

  (ModuleDefinition.FullSanitizedName, DataTypeDecl.FullSanitizedName):
  Use SanitizedName, not CompileName

  (NonglobalVariable.CompilerizeName):
  Rename to SanitizeName

  (NonglobalVariable.AssignUniqueName, LocalVariable.AssignUniqueName):
  Only assign uniqueName (compileName initialization was duplicated with the
  CompileName getter)

  (FunctionCallFinder.PrintFunctionCallGraph):
  Use SanitizedName, not CompileName

  (ModuleDefinition.RefinementCompileName,
   ModuleDefinition.FullSanitizedRefinementName, MemberDecl.FullNameInContext,
   MemberDecl.FullSanitizedRefinementName, SpecialField.FullCompileName,
   SpecialField.FullNameInContext, SpecialField.FullSanitizedRefinementName):
  Remove unused properties

* Source/Dafny/Verifier/Translator.cs (Translator.Translate):
* Source/DafnyServer/SymbolTable.cs (*):

  Use SanitizedName, not CompileName

* Source/Dafny/Resolver.cs (ResolveProgram):
  Use FullSanitizedName instead of FullCompileName when creating a signature for
  an abstract module (originally changed from .Name to .FullCompileName in
  66b9c19)

Fixes #1984.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@cpitclaudel cpitclaudel

Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator)
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

fix: Don't use CompileName outside of the compilers dafny-lang/dafny
1 participant
@cpitclaudel