Skip to content

Commit 5b388dd

Browse files
authored
Name mangling in Python backend considers built-in functions (#6332)
### What was changed? Exactly as it says on the tin. ### How has this been tested? Under `Source/IntegrationTests/TestFiles/LitTests/LitTest/python/`. <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>
1 parent 015bd08 commit 5b388dd

File tree

3 files changed

+32
-3
lines changed

3 files changed

+32
-3
lines changed

Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs

Lines changed: 27 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -61,10 +61,34 @@ string FormatDefaultTypeParameterValue(TopLevelDecl tp) {
6161
protected override string True { get => "True"; }
6262
protected override string False { get => "False"; }
6363
protected override string Conj { get => "and"; }
64-
private static readonly IEnumerable<string> Keywords = new HashSet<string> { "False", "None", "True", "and", "as"
64+
private static readonly IEnumerable<string> ReservedNames = new HashSet<string> {
65+
// Keywords
66+
"False", "None", "True", "and", "as"
6567
, "assert", "async", "await", "break", "class", "continue", "def", "del", "enum", "elif", "else", "except"
6668
, "finally", "for", "from", "global", "if", "import", "in", "is", "lambda", "nonlocal", "not", "or", "pass"
67-
, "raise", "return", "try", "while", "with", "yield" };
69+
, "raise", "return", "try", "while", "with", "yield"
70+
,
71+
// Built-in functions
72+
"abs", "aiter", "all", "anext", "any", "ascii"
73+
, "bin", "bool", "breakpoint", "bytearray", "bytes"
74+
, "callable", "chr", "classmethod", "compile", "complex"
75+
, "delattr", "dict", "dir", "divmod"
76+
, "enumerate", "eval", "exec"
77+
, "filter", "float", "format", "frozenset"
78+
, "getattr", "globals"
79+
, "hasattr", "hash", "help", "hex"
80+
, "id", "input", "int", "isinstance", "issubclass", "iter"
81+
, "len", "list", "locals"
82+
, "map", "max", "memoryview", "min"
83+
, "next"
84+
, "object", "oct", "open", "ord"
85+
, "pow", "print", "property"
86+
, "range", "repr", "reversed", "round"
87+
, "set", "setattr", "slice", "sorted", "staticmethod", "str", "sum", "super"
88+
, "tuple", "type"
89+
, "vars"
90+
, "zip"
91+
};
6892
protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) {
6993
wr.WriteLine($"# Dafny program {program.Name} compiled into Python");
7094
if (Options.IncludeRuntime) {
@@ -219,7 +243,7 @@ private void EmitImports(string moduleName, string pythonModuleName, ConcreteSyn
219243
protected override string GetHelperModuleName() => DafnyRuntimeModule;
220244

221245
private static string MangleName(string name) {
222-
if (Keywords.Contains(name)) {
246+
if (ReservedNames.Contains(name)) {
223247
name = $"{name}_";
224248
} else {
225249
while (name.StartsWith("_")) {
Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s"
2+
3+
method Test(len: int, a: seq<int>) {
4+
var len := |a|;
5+
}

Source/IntegrationTests/TestFiles/LitTests/LitTest/python/ReservedNames.dfy.expect

Whitespace-only changes.

0 commit comments

Comments
 (0)