Fix a bug with includes and /useBaseNameForFileName

If /useBasenameForFilename is specified, tokens just contain file names, which
is not enough to locate included files.

Solution based on Rustan's advice.

3 files changed, 23 insertions, 18 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index c4f038d4..8a3bdb0e 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -41,11 +41,11 @@ public static int Parse (string/*!*/ filename, ModuleDecl module, BuiltIns built
   string s;

   if (filename == "stdin.dfy") {

     s = Microsoft.Boogie.ParserHelper.Fill(System.Console.In, new List<string>());

-    return Parse(s, filename, module, builtIns, errors, verifyThisFile);

+    return Parse(s, filename, filename, module, builtIns, errors, verifyThisFile);

   } else {

     using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {

       s = Microsoft.Boogie.ParserHelper.Fill(reader, new List<string>());

-      return Parse(s, DafnyOptions.Clo.UseBaseNameForFileName ? Path.GetFileName(filename) : filename, module, builtIns, errors, verifyThisFile);

+      return Parse(s, filename, DafnyOptions.Clo.UseBaseNameForFileName ? Path.GetFileName(filename) : filename, module, builtIns, errors, verifyThisFile);

     }

   }

 }

@@ -55,12 +55,12 @@ public static int Parse (string/*!*/ filename, ModuleDecl module, BuiltIns built
 /// Returns the number of parsing errors encountered.

 /// Note: first initialize the Scanner.

 ///</summary>

-public static int Parse (string/*!*/ s, string/*!*/ filename, ModuleDecl module, BuiltIns builtIns, bool verifyThisFile=true) {

+public static int Parse (string/*!*/ s, string/*!*/ fullFilename, string/*!*/ filename, ModuleDecl module, BuiltIns builtIns, bool verifyThisFile=true) {

   Contract.Requires(s != null);

   Contract.Requires(filename != null);

   Contract.Requires(module != null);

   Errors errors = new Errors();

-  return Parse(s, filename, module, builtIns, errors, verifyThisFile);

+  return Parse(s, fullFilename, filename, module, builtIns, errors, verifyThisFile);

 }

 ///<summary>

 /// Parses top-level things (modules, classes, datatypes, class members)

@@ -68,15 +68,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, ModuleDecl module,
 /// Returns the number of parsing errors encountered.

 /// Note: first initialize the Scanner with the given Errors sink.

 ///</summary>

-public static int Parse (string/*!*/ s, string/*!*/ filename, ModuleDecl module, BuiltIns builtIns,

-                         Errors/*!*/ errors, bool verifyThisFile=true) {

+public static int Parse (string/*!*/ s, string/*!*/ fullFilename, string/*!*/ filename, ModuleDecl module,

+                         BuiltIns builtIns, Errors/*!*/ errors, bool verifyThisFile=true) {

   Contract.Requires(s != null);

   Contract.Requires(filename != null);

   Contract.Requires(module != null);

   Contract.Requires(errors != null);

   byte[]/*!*/ buffer = cce.NonNull( UTF8Encoding.Default.GetBytes(s));

   MemoryStream ms = new MemoryStream(buffer,false);

-  Scanner scanner = new Scanner(ms, errors, filename);

+  Scanner scanner = new Scanner(ms, errors, fullFilename, filename);

   Parser parser = new Parser(scanner, errors, module, builtIns, verifyThisFile);

   parser.Parse();

   return parser.errors.count;

@@ -506,7 +506,7 @@ Dafny
      Contract.Assert(defaultModule != null);

   .)

   { "include" stringToken               (. {

-                                             string parsedFile = t.filename;

+                                             string parsedFile = scanner.FullFilename;

                                              bool isVerbatimString;

                                              string includedFile = Util.RemoveParsedStringQuotes(t.val, out isVerbatimString);

                                              includedFile = Util.RemoveEscaping(includedFile, isVerbatimString);

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index d50a4dd6..dae1b95e 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -112,11 +112,11 @@ public static int Parse (string/*!*/ filename, ModuleDecl module, BuiltIns built
   string s;

   if (filename == "stdin.dfy") {

     s = Microsoft.Boogie.ParserHelper.Fill(System.Console.In, new List<string>());

-    return Parse(s, filename, module, builtIns, errors, verifyThisFile);

+    return Parse(s, filename, filename, module, builtIns, errors, verifyThisFile);

   } else {

     using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {

       s = Microsoft.Boogie.ParserHelper.Fill(reader, new List<string>());

-      return Parse(s, DafnyOptions.Clo.UseBaseNameForFileName ? Path.GetFileName(filename) : filename, module, builtIns, errors, verifyThisFile);

+      return Parse(s, filename, DafnyOptions.Clo.UseBaseNameForFileName ? Path.GetFileName(filename) : filename, module, builtIns, errors, verifyThisFile);

     }

   }

 }

@@ -126,12 +126,12 @@ public static int Parse (string/*!*/ filename, ModuleDecl module, BuiltIns built
 /// Returns the number of parsing errors encountered.

 /// Note: first initialize the Scanner.

 ///</summary>

-public static int Parse (string/*!*/ s, string/*!*/ filename, ModuleDecl module, BuiltIns builtIns, bool verifyThisFile=true) {

+public static int Parse (string/*!*/ s, string/*!*/ fullFilename, string/*!*/ filename, ModuleDecl module, BuiltIns builtIns, bool verifyThisFile=true) {

   Contract.Requires(s != null);

   Contract.Requires(filename != null);

   Contract.Requires(module != null);

   Errors errors = new Errors();

-  return Parse(s, filename, module, builtIns, errors, verifyThisFile);

+  return Parse(s, fullFilename, filename, module, builtIns, errors, verifyThisFile);

 }

 ///<summary>

 /// Parses top-level things (modules, classes, datatypes, class members)

@@ -139,15 +139,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, ModuleDecl module,
 /// Returns the number of parsing errors encountered.

 /// Note: first initialize the Scanner with the given Errors sink.

 ///</summary>

-public static int Parse (string/*!*/ s, string/*!*/ filename, ModuleDecl module, BuiltIns builtIns,

-                         Errors/*!*/ errors, bool verifyThisFile=true) {

+public static int Parse (string/*!*/ s, string/*!*/ fullFilename, string/*!*/ filename, ModuleDecl module,

+                         BuiltIns builtIns, Errors/*!*/ errors, bool verifyThisFile=true) {

   Contract.Requires(s != null);

   Contract.Requires(filename != null);

   Contract.Requires(module != null);

   Contract.Requires(errors != null);

   byte[]/*!*/ buffer = cce.NonNull( UTF8Encoding.Default.GetBytes(s));

   MemoryStream ms = new MemoryStream(buffer,false);

-  Scanner scanner = new Scanner(ms, errors, filename);

+  Scanner scanner = new Scanner(ms, errors, fullFilename, filename);

   Parser parser = new Parser(scanner, errors, module, builtIns, verifyThisFile);

   parser.Parse();

   return parser.errors.count;

@@ -536,7 +536,7 @@ bool IsType(ref IToken pt) {
 			Get();

 			Expect(20);

 			{

-			 string parsedFile = t.filename;

+			 string parsedFile = scanner.FullFilename;

 			 bool isVerbatimString;

 			 string includedFile = Util.RemoveParsedStringQuotes(t.val, out isVerbatimString);

 			 includedFile = Util.RemoveEscaping(includedFile, isVerbatimString);

diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index 325a2f2c..a73f510d 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -224,6 +224,7 @@ public class Scanner {
 		Contract.Invariant(pt != null);

 		Contract.Invariant(tval != null);

 		Contract.Invariant(Filename != null);

+		Contract.Invariant(FullFilename != null);

 		Contract.Invariant(errorHandler != null);

 	}

 

@@ -258,6 +259,8 @@ public class Scanner {
 	private string/*!*/ Filename;

 	private Errors/*!*/ errorHandler;

 

+	internal string/*!*/ FullFilename { get; private set; }

+

 	static Scanner() {

 		start = new Hashtable(128);

 		for (int i = 63; i <= 63; ++i) start[i] = 1;

@@ -310,7 +313,7 @@ public class Scanner {
 	}

 

 //	[NotDelayed]

-	public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler, bool useBaseName = false) : base() {

+	public Scanner (string/*!*/ fullFilename, string/*!*/ fileName, Errors/*!*/ errorHandler, bool useBaseName = false) : base() {

 	  Contract.Requires(fileName != null);

 	  Contract.Requires(errorHandler != null);

 		this.errorHandler = errorHandler;

@@ -319,6 +322,7 @@ public class Scanner {
 		try {

 			Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);

 			this._buffer = new Buffer(stream, false);

+			this.FullFilename = fullFilename;

 			Filename = useBaseName? GetBaseName(fileName): fileName;

 			Init();

 		} catch (IOException) {

@@ -327,7 +331,7 @@ public class Scanner {
 	}

 

 //	[NotDelayed]

-	public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName, bool useBaseName = false) : base() {

+	public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fullFilename, string/*!*/ fileName, bool useBaseName = false) : base() {

 	  Contract.Requires(s != null);

 	  Contract.Requires(errorHandler != null);

 	  Contract.Requires(fileName != null);

@@ -335,6 +339,7 @@ public class Scanner {
 		t = new Token(); // dummy because t is a non-null field

 		this._buffer = new Buffer(s, true);

 		this.errorHandler = errorHandler;

+		this.FullFilename = fullFilename;

 		this.Filename = useBaseName? GetBaseName(fileName) : fileName;

 		Init();

 	}