Fixed problem where Dafny filenames with unusual characters in filenames had caused malformed Boogie and malformed VCs. In particular, the problem arose in the CEV $file_name_is declarations. Such characters are now replaced by a percent sign followed by a four-digit hexadecimal number representing the Unicode value of the character.

This fixes issue #6057.

1 files changed, 13 insertions, 1 deletions

diff --git a/Dafny/Translator.ssc b/Dafny/Translator.ssc
index 64401071..d47c25a2 100644
--- a/Dafny/Translator.ssc
+++ b/Dafny/Translator.ssc
@@ -7,6 +7,7 @@ using System;
 using System.Collections.Generic;

 using Microsoft.Contracts;

 using Bpl = Microsoft.Boogie;

+using System.Text;

 

 // TODO:  wellformedness checks for function bodies

 // TODO:  totality checks for statements

@@ -49,7 +50,7 @@ namespace Microsoft.Dafny {
         if (!cevFilenames.TryGetValue(filename, out fileId)) {

           fileId = cevFilenames.Count;

           cevFilenames.Add(filename, fileId);

-          Bpl.Constant fn = new Bpl.Constant(tok, new Bpl.TypedIdent(tok, filename, predef.CevTokenType), true);

+          Bpl.Constant fn = new Bpl.Constant(tok, new Bpl.TypedIdent(tok, Sanitize(filename), predef.CevTokenType), true);

           sink.TopLevelDeclarations.Add(fn);

           sink.TopLevelDeclarations.Add(new Bpl.Axiom(tok, FunctionCall(tok, "$file_name_is", Bpl.Type.Bool, Bpl.Expr.Literal(fileId), new Bpl.IdentifierExpr(tok, fn))));

         }

@@ -59,6 +60,17 @@ namespace Microsoft.Dafny {
       }

       return new Bpl.IdentifierExpr(tok, c);

     }

+    static string! Sanitize(string! s) {

+      StringBuilder sb = new StringBuilder();

+      foreach (char ch in s) {

+        if (char.IsLetterOrDigit(ch) || ch == '#' || ch == '^' || ch == '$' || ch == '.' || ch == '@') {

+          sb.Append(ch);

+        } else {

+          sb.Append(string.Format("%{0:X4}", (int)ch));

+        }

+      }

+      return sb.ToString();

+    }

     Bpl.Expr! CevVariable(Bpl.IToken! tok, string! name)

       requires predef != null && sink != null;

     {