Parser error in IfStatement parsing

jennalwise commented 2 years ago

This lemma function in list.c0 is not parsing:

void appendLemma(struct Node *a, struct Node *b, struct Node *c)
  //@ sortedSeg(a, b) && sortedSeg(b, c)
  //@ sortedSeg(a, c)
{
  if (a == b) {
  } else {
    //@ unfold sortedSeg(a, b);
    appendLemma(a->next, b, c);
    //@ fold sortedSeg(a, c);
  }
}

The parser outputs the following error:

sbt:gvc0> run src/test/resources/quant-study/list.c0
[info] running (fork) gvc.Main src/test/resources/quant-study/list.c0
[info] Verifying 1 file(s)
[info] Parse error in 'src/test/resources/quant-study/list.c0':
[info] Expected program:1:1 / definition:39:1 / methodDefinition:39:1 / blockStatement:42:1 / span:42:1 / statement:43:3 / concreteStatement:43:3 / ifStatement:43:3 / span:43:3 / statement:44:10 / concreteStatement:44:10 / blockStatement:44:10 / span:44:10 / statement:47:5 / concreteStatement:48:3 / (annotation | blockStatement | ifStatement | whileStatement | forStatement | returnStatement | assertStatement | errorStatement | simpleStatement):48:3, found "}\n}\n\nstruc"
[error] Nonzero exit code returned from runner: 2
[error] (Compile / run) Nonzero exit code returned from runner: 2
[error] Total time: 10 s, completed Oct 11, 2021, 8:52:29 PM

Alternates that parse without error:

void appendLemma(struct Node *a, struct Node *b, struct Node *c)
  //@ sortedSeg(a, b) && sortedSeg(b, c)
  //@ sortedSeg(a, c)
{
  if (a == b) {
  } else {
    //@ unfold sortedSeg(a, b);
    appendLemma(a->next, b, c);
  }
}

void appendLemma(struct Node *a, struct Node *b, struct Node *c)
  //@ sortedSeg(a, b) && sortedSeg(b, c)
  //@ sortedSeg(a, c)
{
  if (a == b) {
  } else {
    //@ unfold sortedSeg(a, b);
    //@ fold sortedSeg(a, c);
  }
}

int appendLemma(struct Node *a, struct Node *b, struct Node *c)
  //@ sortedSeg(a, b) && sortedSeg(b, c)
  //@ sortedSeg(a, c)
{
  if (a == b) {
  } else {
    //@ unfold sortedSeg(a, b);
    appendLemma(a->next, b, c);
    //@ fold sortedSeg(a, c);
    return 0;
  }
  return 0;
}

This also does not parse with a similar error:

int appendLemma(struct Node *a, struct Node *b, struct Node *c)
  //@ sortedSeg(a, b) && sortedSeg(b, c)
  //@ sortedSeg(a, c)
{
  if (a == b) {
  } else {
    //@ unfold sortedSeg(a, b);
    appendLemma(a->next, b, c);
    //@ fold sortedSeg(a, c);
  }
  return 0;
}

Something weird is going on when parsing the else case of an if with the given program statements. I tried to debug it further, but I couldn't find any issues, not that I really have enough understanding of the parser implementation at this time to debug it that well. I will try to debug it some other time. But, right now I am moving forward with a version that parses and contains the semantics I am looking for.

conradz commented 2 years ago

I believe this a bug that happens when any spec statement (i.e. a //@ statement) occurs after a "regular" (non-spec) C0 statement and right before the close of a block.

Here is a minimal example that currently fails to parse:

void abc()
{
  assert(true);
  //@assert true;
}

jennalwise commented 2 years ago

Makes sense from my experience that this is the issue!

gradual-verification / gvc0

Parser error in IfStatement parsing #9