Improve error reporting for some parsing and typechecking errors

[JonasAlaif]

I've added cuts in various places in the parser (notably in exp). This caused issues with parsing [exp] vs [exp..] (using ("[" ~ exp ~ ".." ~ Pass ~ "]") | ("[" ~ exp ~ "]") | ... caused the cut in the first case to prevent backtracking and getting to the other case, this should also be avoided in general see Avoid Backtracking) which had to be fixed.

I also changed the duplicate identifier error to instead use the span of the found duplicate rather than the first declaration.

If there aren't any major issues, can we merge this before the release @marcoeilers?

[JonasAlaif]

Maybe you already knew this, but using .log on parsers is extremely useful for debugging

[marcoeilers]

Thanks!
I'm not super convinced we should merge this before the release because the parser has some bad parts that essentially rely on backtracking to work. For example, this does not parse any more:

domain huh {
    function myfun(b: Bool): Bool

}

method m()
{
  assert (myfun(forall i: Int :: i > 0 || i <= 0))
}

And I'm not sure we'll find all issues on time.

[JonasAlaif]

True, I didn't have time to rerun the test yesterday and thought that all of them were passing

[JonasAlaif]

@marcoeilers btw this is already an issue in current silver:

domain huh {
    function myfun(b: Bool): Bool
}

method m()
{
  var x: Ref, y: Ref
  inhale acc(x.f) && (acc(x.f) --* acc(y.f))
  assert (myfun(applying (acc(x.f) --* acc(y.f)) in y.f == 0))
}

since applying does the cut that I've added to forall here

[JonasAlaif]

@marcoeilers this is ready to merge

[marcoeilers]

Two files here (https://github.com/viperproject/se_vcg_comparison/tree/main/bench_selection) that should parse don't:

• gobra/wireguard/initiator_main.go.vpr
• gobra/wireguard/responder_main.go.vpr

[JonasAlaif]

@marcoeilers One issue is that

method bar()
{
  a := a
  (foo(): Ref).field := a
}

looks like a function call at the end of the first assign...

[JonasAlaif]

@marcoeilers do you think that it's reasonable to require a function call foo and the initial paren ( to be on the same line? Otherwise e.g. the following is really difficult to parse:

field f: Ref
method bar(a: Ref)
    requires acc(a.f)
{
  // Looks like `var b := a(b).f`
  var b: Ref := a
  (b).f := a
}

[marcoeilers]

My immediate thoughts would be that 1) IMO newlines should be like any other whitespace, but 2) do we need to allow any whitespace before that parenthesis?

[JonasAlaif]

@marcoeilers I'm not sure. The only reason I see for allowing it is for formatting reasons, but I've never seen anyone formatting calls with any whitespace before the (. However, both Scala and Rust allow whitespace incl. newlines. The only reason I suggested banning newline but not space is that I could imagine it could break some existing code. I don't see any other solution to this though, outside of removing all cuts from all expressions. Even the cuts in the current parser cause issues, e.g. the following with Viper main fails to parse:

field f: Bool
method bar(a: Bool, b: Seq[Ref])
    requires |b| > 0 && acc(b[0].f)
{
  assume a
  (b[..1][0]).f := a
}

due to a cut after ...

[marcoeilers]

Hm. Might be a topic for the Viper meeting?

[JonasAlaif]

Yep we should discuss it then, for now does the thing I pushed look reasonable? It solves the two parse issues you had

[marcoeilers]

Subsumed by #764