Weaver fails when multiple accessibility predicates for a return value must be run-time checked

[jennalwise]

For this program below,

#use <conio>
#use <stress>

struct MinPriorityQueue;
struct Node;

struct MinPriorityQueue
{
  struct Node* head;
  int size;
};

struct Node
{
  int val;
  struct Node* next;
};

//@predicate foo() = ? && true;

struct MinPriorityQueue* createMinPriQueue(int value);
int main();

struct MinPriorityQueue* createMinPriQueue(int value)
  //@requires true;
  //@ensures acc(\result->head) && acc(\result->size);
{
  struct MinPriorityQueue* q = NULL;
  struct Node* _ = NULL;
  q = alloc(struct MinPriorityQueue);
  _ = alloc(struct Node);
  q->head = _;
  q->head->val = value;
  q->head->next = NULL;
  q->size = 1;  

  //@ fold foo();

  return q;
}

int main()
  //@requires true;
  //@ensures true;
{
  return 0;
}

The verifier outputs this error in the Weaver:

[error] Exception in thread "main" gvc.weaver.WeaverException: Invalid \result expression
[error]         at gvc.Main$.verifySiliconProvided(main.scala:311)
[error]         at gvc.Main$.verify(main.scala:259)
[error]         at gvc.Main$.$anonfun$run$4(main.scala:153)
[error]         at gvc.benchmarking.Output$.printTiming(Output.scala:47)
[error]         at gvc.Main$.run(main.scala:152)
[error]         at gvc.Main$.delayedEndpoint$gvc$Main$1(main.scala:72)
[error]         at gvc.Main$delayedInit$body.apply(main.scala:41)
[error]         at scala.Function0.apply$mcV$sp(Function0.scala:39)
[error]         at scala.Function0.apply$mcV$sp$(Function0.scala:39)
[error]         at scala.runtime.AbstractFunction0.apply$mcV$sp(AbstractFunction0.scala:17)
[error]         at scala.App.$anonfun$main$1$adapted(App.scala:80)
[error]         at scala.collection.immutable.List.foreach(List.scala:431)
[error]         at scala.App.main(App.scala:80)
[error]         at scala.App.main$(App.scala:78)
[error]         at gvc.Main$.main(main.scala:41)
[error]         at gvc.Main.main(main.scala)
[error] Nonzero exit code returned from runner: 1
[error] (Compile / run) Nonzero exit code returned from runner: 1
[error] Total time: 9 s, completed Aug 1, 2023, 8:27:39 PM

It is because there are 2 run-time checks for accessibility predicates containing \result in them. When I remove any one of the accessibility predicates from the postcondition, the error doesn't occur. Same error happens if one of the accessibility predicates is replaced by a predicate that takes \result as an argument.

[jennalwise]

Same error pops up in stack-list.c0 where \result is used in a logical conditional run-time check:

bool isEmpty(struct Stack* s)
  //@requires ?;
  //@ensures ? && (\result == true ? true : nonEmptyStack(s));
{
  if (s == NULL)
  {
    return true;
  }
  else
  {
    if (s->top == NULL)
    {
      return true;
    }
    else
    {
      return false;
    }
  }
}

[jennalwise]

Some more information from debugging:

• The errors are coming from separation checks like RuntimeCheck(MethodPost,FieldSeparationCheck(Field(Result,MinPriorityQueue,size)),None) containing result in conditions
• The interesting thing is that the corresponding "logic" check is okay as it uses the actual check value from the verifier (result is in the AST context): RuntimeCheck(MethodPost,FieldAccessibilityCheck(Field(Var(q),MinPriorityQueue,size)),None)

This happens similarly in the second example.

It turns out all the checks are not marked as conditions except for the last one:

[OKAY] RuntimeCheck(MethodPost,FieldAccessibilityCheck(Field(Var(q),MinPriorityQueue,head)),None)
[OKAY] RuntimeCheck(MethodPost,FieldAccessibilityCheck(Field(Var(q),MinPriorityQueue,size)),None)
[OKAY] RuntimeCheck(MethodPost,FieldSeparationCheck(Field(Result,MinPriorityQueue,head)),None)
[MARKED AS CONDITION] RuntimeCheck(MethodPost,FieldSeparationCheck(Field(Result,MinPriorityQueue,size)),None)

None of them should be marked as condition in the first example.

Of course in the second example there are conditions to analyze with result: The logic check RuntimeCheck(MethodPost,PredicateAccessibilityCheck(nonEmptyStack,List(Var(s))),Some(NotCondition(ImmediateCondition(Eq(FalseLit,TrueLit))))) uses the direct condition value from the verifier !(false == true)

The separation check RuntimeCheck(MethodPost,PredicateSeparationCheck(nonEmptyStack,List(Var(s))),Some(ImmediateCondition(Not(Eq(Result,TrueLit))))) uses the context subbed into the direct condition aka !(result == true). The logic check succeeds and the separation check fails when the condition is sent to expr.toIR with the returnValue set to None always.