fix: ensure postcondition expression is extracted from the right URI

[dijkstracula]

The following bug requires two Dafny files, one containing an abstract module and another one refining it, like these:

$ ls -l
total 16
-rw-r--r--  1 ntaylor  staff   81 Nov 10 14:25 module.dfy
-rw-r--r--  1 ntaylor  staff  113 Nov 10 14:25 repro.dfy

$ cat repro.dfy
include "./module.dfy"

module Repro refines M {
    function method Foo(n: nat): nat
    {
        n + 1
    }
}%            
                                                                                                                                                                    
$ cat module.dfy
module M {
    function method Foo(n: nat): nat
        ensures Foo(n) % 2 == 0
}%                                                                                                                                                                                ➜  dafny_repo

The command line tool gives reasonable output: it indicates that a postcondition might not hold, and points to the ensures in the abstract module by indicating the file, line, and column value:

➜  dafny_repo ~/code/dafny/Binaries/Dafny repro.dfy
/Users/ntaylor/school/dafny_repo/repro.dfy(4,20): Error: A postcondition might not hold on this return path.
/Users/ntaylor/school/dafny_repo/./module.dfy(3,27): Related location: This is the postcondition that might not hold.

Dafny program verifier finished with 0 verified, 1 error
➜  dafny_repo

However, the language server attempts to concretise the postcondition by slicing a substring out of the failing program source. The server assumes that the postcondition is in the current document - in the case of module refinement, this isn't the case. Thus, we get a nonsensical error:

[{
	"resource": "/Users/ntaylor/school/dafny_repo/repro.dfy",
...
	"relatedInformation": [
		{
			"startLineNumber": 3,
			"startColumn": 17,
			"endLineNumber": 3,
			"endColumn": 32,
			"message": "This postcondition might not hold: thod Foo(n: nat",
			"resource": "/Users/ntaylor/school/dafny_repo/./module.dfy"
...
}]

Those are, of course, the characters corresponding to the postcondition, but in the current file, not the file that actually contains it! (one can add or remove characters early on in the file and watch the garbage postcondition "slide around").

This patch ensures that when extracting substrings from a document, the right URI is used. (This patch cleans up a bit of the existing logic: there was a "default" error message for the "Related location" case that would never get hit, etc)

[{
	"resource": "/Users/ntaylor/school/dafny_repo/repro.dfy",
...
	"relatedInformation": [
		{
...
			"message": "This postcondition might not hold: Foo(n) % 2 == 0",
			"resource": "/Users/ntaylor/school/dafny_repo/./module.dfy"
		}
	]
}]

I will push another commit with the release notes modified, once I create this pull request and am assigned a PR number from GitHub.

Additionally: I'm not sure how to write a git-issue test for this, since two Dafny files are required to trigger the issue. What would you like me to do?

Cheers,
Nathan